feat(builtin/kernel): use the same notation for mp, eq::mp and forall::elim

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

examples/lean/ex5.lean

@@ -16,8 +16,8 @@ pop::scope
 
 scope
   -- Same example but using ∀ instead of Π and ⇒ instead of →.
-  -- Remark: H ↓ x   is syntax sugar for forall::elim H x
-  -- Remark: H1 ◂ H2 is syntax sugar for mp H1 H2
+  -- Remark: H ◂ x   is syntax sugar for forall::elim H x,
+  -- and H1 ◂ H2 is syntax sugar for mp H1 H2
   theorem ReflIf (A : Type)
                  (R : A → A → Bool)
                  (Symm : ∀ x y, R x y ⇒ R y x)
@@ -25,9 +25,9 @@ scope
                  (Linked : ∀ x, ∃ y, R x y)
                  :
                  ∀ x, R x x :=
-    take x, obtain (w : A) (H : R x w), from (Linked ↓ x),
-       let L1 : R w x := Symm ↓ x ↓ w ◂ H
-       in Trans ↓ x ↓ w ↓ x ◂ H ◂ L1
+    take x, obtain (w : A) (H : R x w), from (Linked ◂ x),
+       let L1 : R w x := Symm ◂ x ◂ w ◂ H
+       in Trans ◂ x ◂ w ◂ x ◂ H ◂ L1
 
 pop::scope
 

examples/lean/set.lean

@@ -13,25 +13,25 @@ theorem subset::trans (A : Type) : ∀ s1 s2 s3 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s3
       have s1 ⊆ s3 :
         take x, assume Hin : x ∈ s1,
            have x ∈ s3 :
-             let L1 : x ∈ s2 := H1 ↓ x ◂ Hin
-             in H2 ↓ x ◂ L1
+             let L1 : x ∈ s2 := H1 ◂ x ◂ Hin
+             in H2 ◂ x ◂ L1
 
 theorem subset::ext (A : Type) : ∀ s1 s2 : Set A, (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 :=
    take s1 s2, assume (H : ∀ x, x ∈ s1 = x ∈ s2),
-       abst (λ x, H ↓ x)
+       abst (λ x, H ◂ x)
 
 theorem subset::antisym (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 :=
    take s1 s2, assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1),
        have s1 = s2 :
             (have (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 :
-                  (subset::ext A) ↓ s1 ↓ s2)
+                  (subset::ext A) ◂ s1 ◂ s2)
             ◂ (have (∀ x, x ∈ s1 = x ∈ s2) :
                     take x, have x ∈ s1 = x ∈ s2 :
-                       iff::intro (have x ∈ s1 ⇒ x ∈ s2 : H1 ↓ x)
-                                  (have x ∈ s2 ⇒ x ∈ s1 : H2 ↓ x))
+                       iff::intro (have x ∈ s1 ⇒ x ∈ s2 : H1 ◂ x)
+                                  (have x ∈ s2 ⇒ x ∈ s1 : H2 ◂ x))
 
 
 -- Compact (but less readable) version of the previous theorem
 theorem subset::antisym2 (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 :=
    take s1 s2, assume H1 H2,
-     (subset::ext A) ↓ s1 ↓ s2 ◂ (take x, iff::intro (H1 ↓ x) (H2 ↓ x))
+     (subset::ext A) ◂ s1 ◂ s2 ◂ (take x, iff::intro (H1 ◂ x) (H2 ◂ x))

src/builtin/Nat.lean

@@ -207,10 +207,10 @@ theorem plus::eqz {a b : Nat} (H : a + b = 0) : a = 0
                              ...  ≠  0           : succ::nz (n + b)))
 
 theorem le::intro {a b c : Nat} (H : a + c = b) : a ≤ b
-:= (symm (le::def a b)) ◆ (have (∃ x, a + x = b) : exists::intro c H)
+:= (symm (le::def a b)) ◂ (have (∃ x, a + x = b) : exists::intro c H)
 
 theorem le::elim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b
-:= (le::def a b) ◆ H
+:= (le::def a b) ◂ H
 
 theorem le::refl (a : Nat) : a ≤ a := le::intro (plus::zeror a)
 

src/builtin/kernel.lean

@@ -105,8 +105,8 @@ theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false
 theorem eq::mp {a b : Bool} (H1 : a == b) (H2 : a) : b
 := subst H2 H1
 
-infixl 100 <|> : eq::mp
-infixl 100 ◆   : eq::mp
+infixl 100 <| : eq::mp
+infixl 100 ◂  : eq::mp
 
 -- assume is a 'macro' that expands into a discharge
 
@@ -114,16 +114,16 @@ theorem imp::trans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c
 := assume Ha, H2 ◂ (H1 ◂ Ha)
 
 theorem imp::eq::trans {a b c : Bool} (H1 : a ⇒ b) (H2 : b == c) : a ⇒ c
-:= assume Ha, H2 ◆ (H1 ◂ Ha)
+:= assume Ha, H2 ◂ (H1 ◂ Ha)
 
 theorem eq::imp::trans {a b c : Bool} (H1 : a == b) (H2 : b ⇒ c) : a ⇒ c
-:= assume Ha, H2 ◂ (H1 ◆ Ha)
+:= assume Ha, H2 ◂ (H1 ◂ Ha)
 
 theorem not::not::eq (a : Bool) : (¬ ¬ a) == a
 := case (λ x, (¬ ¬ x) == x) trivial trivial a
 
 theorem not::not::elim {a : Bool} (H : ¬ ¬ a) : a
-:= (not::not::eq a) ◆ H
+:= (not::not::eq a) ◂ H
 
 theorem mt {a b : Bool} (H1 : a ⇒ b) (H2 : ¬ b) : ¬ a
 := assume H : a, absurd (H1 ◂ H) H2
@@ -193,7 +193,7 @@ theorem ne::eq::trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a
 := subst H1 H2
 
 theorem eqt::elim {a : Bool} (H : a == true) : a
-:= (symm H) ◆ trivial
+:= (symm H) ◂ trivial
 
 theorem eqt::intro {a : Bool} (H : a) : a == true
 := iff::intro (assume H1 : a, trivial)
@@ -218,8 +218,8 @@ theorem congr {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} {a b : A} (H1
 theorem forall::elim {A : TypeU} {P : A → Bool} (H : Forall A P) (a : A) : P a
 := eqt::elim (congr1 a H)
 
-infixl 100 ! : forall::elim
-infixl 100 ↓ : forall::elim
+infixl 100 <| : forall::elim
+infixl 100 ◂  : forall::elim
 
 theorem forall::intro {A : TypeU} {P : A → Bool} (H : Π x : A, P x) : Forall A P
 := (symm (eta P)) ⋈ (abst (λ x, eqt::intro (H x)))
@@ -322,7 +322,7 @@ theorem not::and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b)
         a
 
 theorem not::and::elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b
-:= (not::and a b) ◆ H
+:= (not::and a b) ◂ H
 
 theorem not::or (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b)
 := case (λ x, (¬ (x ∨ b)) == (¬ x ∧ ¬ b))
@@ -331,7 +331,7 @@ theorem not::or (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b)
         a
 
 theorem not::or::elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b
-:= (not::or a b) ◆ H
+:= (not::or a b) ◂ H
 
 theorem not::iff (a b : Bool) : (¬ (a == b)) == ((¬ a) == b)
 := case (λ x, (¬ (x == b)) == ((¬ x) == b))
@@ -340,7 +340,7 @@ theorem not::iff (a b : Bool) : (¬ (a == b)) == ((¬ a) == b)
         a
 
 theorem not::iff::elim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b
-:= (not::iff a b) ◆ H
+:= (not::iff a b) ◂ H
 
 theorem not::implies (a b : Bool) : (¬ (a ⇒ b)) == (a ∧ ¬ b)
 := case (λ x, (¬ (x ⇒ b)) == (x ∧ ¬ b))
@@ -349,7 +349,7 @@ theorem not::implies (a b : Bool) : (¬ (a ⇒ b)) == (a ∧ ¬ b)
         a
 
 theorem not::implies::elim {a b : Bool} (H : ¬ (a ⇒ b)) : a ∧ ¬ b
-:= (not::implies a b) ◆ H
+:= (not::implies a b) ◂ H
 
 theorem not::congr {a b : Bool} (H : a == b) : (¬ a) == (¬ b)
 := congr2 not H
@@ -365,14 +365,14 @@ theorem not::forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (
                    ...    = (∃ x : A, ¬ P x)      : refl (∃ x : A, ¬ P x)
 
 theorem not::forall::elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x
-:= (not::forall A P) ◆ H
+:= (not::forall A P) ◂ H
 
 theorem not::exists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) == (∀ x : A, ¬ P x)
 := calc (¬ ∃ x : A, P x) = (¬ ¬ ∀ x : A, ¬ P x) : refl (¬ ∃ x : A, P x)
                      ... = (∀ x : A, ¬ P x)     : not::not::eq (∀ x : A, ¬ P x)
 
 theorem not::exists::elim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x
-:= (not::exists A P) ◆ H
+:= (not::exists A P) ◂ H
 
 theorem exists::unfold1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x)
 := exists::elim H

tests/lean/mp_forallelim.lean

@@ -0,0 +1,7 @@
+variable p : Nat -> Nat -> Bool
+check fun (a b c : Bool) (p : Nat -> Nat -> Bool) (n m : Nat)
+          (H : a => b => (forall x y, c => p (x + n) (x + m)))
+          (Ha : a)
+          (Hb : b)
+          (Hc : c),
+          H ◂ Ha ◂ Hb ◂ 0 ◂ 1 ◂ Hc

tests/lean/mp_forallelim.lean.expected.out

@@ -0,0 +1,13 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: p
+λ (a b c : Bool)
+  (p : ℕ → ℕ → Bool)
+  (n m : ℕ)
+  (H : a ⇒ b ⇒ (∀ x y : ℕ, c ⇒ p (x + n) (x + m)))
+  (Ha : a)
+  (Hb : b)
+  (Hc : c),
+  H ◂ Ha ◂ Hb ◂ 0 ◂ 1 ◂ Hc :
+    Π (a b c : Bool) (p : ℕ → ℕ → Bool) (n m : ℕ),
+      (a ⇒ b ⇒ (∀ x y : ℕ, c ⇒ p (x + n) (x + m))) → a → b → c → p (0 + n) (0 + m)

tests/lean/tst3.lean.expected.out

@@ -7,11 +7,6 @@ implies ⊤ (implies a ⊥)
 notation 100 _ |- _ ; _ : f
 f c d e
 c |- d ; e
-Notation has been redefined, the existing notation:
-  infixl 100 !
-has been replaced with:
-  notation 20 _ !
-because they conflict with each other.
 (c !) !
 fact (fact c)
 The precedence of ';' changed from 100 to 30.