diff --git a/examples/lean/ex2.lean b/examples/lean/ex2.lean index 341cfcc32b..cafdd0d1cb 100644 --- a/examples/lean/ex2.lean +++ b/examples/lean/ex2.lean @@ -1,7 +1,7 @@ Import macros. Theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r -:= assume H_pq_qr H_p, +:= Assume H_pq_qr H_p, let P_pq := Conjunct1 H_pq_qr, P_qr := Conjunct2 H_pq_qr, P_q := MP P_pq H_p @@ -11,7 +11,7 @@ SetOption pp::implicit true. Show Environment 1. Theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c -:= assume H_abc H_ab H_a, +:= Assume H_abc H_ab H_a, let P_b := (MP H_ab H_a), P_bc := (MP H_abc H_a) in MP P_bc P_b. diff --git a/examples/lean/ex3.lean b/examples/lean/ex3.lean index 1cebe33b9f..5d4c60b0de 100644 --- a/examples/lean/ex3.lean +++ b/examples/lean/ex3.lean @@ -1,10 +1,10 @@ Import macros. Theorem and_comm (a b : Bool) : (a ∧ b) ⇒ (b ∧ a) -:= assume H_ab, Conj (Conjunct2 H_ab) (Conjunct1 H_ab). +:= Assume H_ab, Conj (Conjunct2 H_ab) (Conjunct1 H_ab). Theorem or_comm (a b : Bool) : (a ∨ b) ⇒ (b ∨ a) -:= assume H_ab, +:= Assume H_ab, DisjCases H_ab (λ H_a, Disj2 b H_a) (λ H_b, Disj1 H_b a). @@ -23,7 +23,7 @@ produces a ----------------------------------- *) Theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a -:= assume H, DisjCases (EM a) +:= Assume H, DisjCases (EM a) (λ H_a, H_a) (λ H_na, NotImp1 (MT H H_na)). diff --git a/examples/lean/set.lean b/examples/lean/set.lean index 45e9d72590..fb0da85185 100644 --- a/examples/lean/set.lean +++ b/examples/lean/set.lean @@ -9,30 +9,30 @@ Definition subset {A : Type} (s1 : Set A) (s2 : Set A) := ∀ x, x ∈ s1 ⇒ x Infix 50 ⊆ : subset Theorem SubsetTrans (A : Type) : ∀ s1 s2 s3 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s3 ⇒ s1 ⊆ s3 := - for s1 s2 s3, assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3), + For s1 s2 s3, Assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3), show s1 ⊆ s3, - for x, assume Hin : x ∈ s1, + For x, Assume Hin : x ∈ s1, show x ∈ s3, - let L1 : x ∈ s2 := mp (instantiate H1 x) Hin - in mp (instantiate H2 x) L1 + let L1 : x ∈ s2 := MP (Instantiate H1 x) Hin + in MP (Instantiate H2 x) L1 Theorem SubsetExt (A : Type) : ∀ s1 s2 : Set A, (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2 := - for s1 s2, assume (H : ∀ x, x ∈ s1 = x ∈ s2), - Abst (fun x, instantiate H x) + For s1 s2, Assume (H : ∀ x, x ∈ s1 = x ∈ s2), + Abst (fun x, Instantiate H x) Theorem SubsetAntiSymm (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 := - for s1 s2, assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1), + For s1 s2, Assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1), show s1 = s2, MP (show (∀ x, x ∈ s1 = x ∈ s2) ⇒ s1 = s2, - instantiate (SubsetExt A) s1 s2) + Instantiate (SubsetExt A) s1 s2) (show (∀ x, x ∈ s1 = x ∈ s2), - for x, show x ∈ s1 = x ∈ s2, - let L1 : x ∈ s1 ⇒ x ∈ s2 := instantiate H1 x, - L2 : x ∈ s2 ⇒ x ∈ s1 := instantiate H2 x + For x, show x ∈ s1 = x ∈ s2, + let L1 : x ∈ s1 ⇒ x ∈ s2 := Instantiate H1 x, + L2 : x ∈ s2 ⇒ x ∈ s1 := Instantiate H2 x in ImpAntisym L1 L2) (* Compact (but less readable) version of the previous theorem *) Theorem SubsetAntiSymm2 (A : Type) : ∀ s1 s2 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s1 ⇒ s1 = s2 := - for s1 s2, assume H1 H2, - MP (instantiate (SubsetExt A) s1 s2) - (for x, ImpAntisym (instantiate H1 x) (instantiate H2 x)) + For s1 s2, Assume H1 H2, + MP (Instantiate (SubsetExt A) s1 s2) + (For x, ImpAntisym (Instantiate H1 x) (Instantiate H2 x)) diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index 058eea4dc6..9cd10db95a 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -43,13 +43,13 @@ Theorem ZeroNeOne : 0 ≠ 1 := Trivial. Theorem NeZeroPred' (a : Nat) : a ≠ 0 ⇒ ∃ b, b + 1 = a := Induction a - (assume H : 0 ≠ 0, FalseElim (∃ b, b + 1 = 0) H) + (Assume H : 0 ≠ 0, FalseElim (∃ b, b + 1 = 0) H) (λ (n : Nat) (iH : n ≠ 0 ⇒ ∃ b, b + 1 = n), - assume H : n + 1 ≠ 0, + Assume H : n + 1 ≠ 0, DisjCases (EM (n = 0)) (λ Heq0 : n = 0, ExistsIntro 0 (calc 0 + 1 = n + 1 : { Symm Heq0 })) (λ Hne0 : n ≠ 0, - obtain (w : Nat) (Hw : w + 1 = n), from (MP iH Hne0), + Obtain (w : Nat) (Hw : w + 1 = n), from (MP iH Hne0), ExistsIntro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw }))). Theorem NeZeroPred {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a @@ -58,7 +58,7 @@ Theorem NeZeroPred {a : Nat} (H : a ≠ 0) : ∃ b, b + 1 = a Theorem Destruct {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : Π n, a = n + 1 → B) : B := DisjCases (EM (a = 0)) (λ Heq0 : a = 0, H1 Heq0) - (λ Hne0 : a ≠ 0, obtain (w : Nat) (Hw : w + 1 = a), from (NeZeroPred Hne0), + (λ Hne0 : a ≠ 0, Obtain (w : Nat) (Hw : w + 1 = a), from (NeZeroPred Hne0), H2 w (Symm Hw)). Theorem ZeroPlus (a : Nat) : 0 + a = a @@ -178,12 +178,12 @@ Theorem MulAssoc (a b c : Nat) : a * (b * c) = a * b * c Theorem PlusInj' (a b c : Nat) : a + b = a + c ⇒ b = c := Induction a - (assume H : 0 + b = 0 + c, + (Assume H : 0 + b = 0 + c, calc b = 0 + b : Symm (ZeroPlus b) ... = 0 + c : H ... = c : ZeroPlus c) (λ (n : Nat) (iH : n + b = n + c ⇒ b = c), - assume H : n + 1 + b = n + 1 + c, + Assume H : n + 1 + b = n + 1 + c, let L1 : n + b + 1 = n + c + 1 := (calc n + b + 1 = n + (b + 1) : Symm (PlusAssoc n b 1) ... = n + (1 + b) : { PlusComm b 1 } @@ -219,22 +219,22 @@ Theorem LeRefl (a : Nat) : a ≤ a := LeIntro (PlusZero a). Theorem LeZero (a : Nat) : 0 ≤ a := LeIntro (ZeroPlus a). Theorem LeTrans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c -:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (LeElim H1), - obtain (w2 : Nat) (Hw2 : b + w2 = c), from (LeElim H2), +:= Obtain (w1 : Nat) (Hw1 : a + w1 = b), from (LeElim H1), + Obtain (w2 : Nat) (Hw2 : b + w2 = c), from (LeElim H2), LeIntro (calc a + (w1 + w2) = a + w1 + w2 : PlusAssoc a w1 w2 ... = b + w2 : { Hw1 } ... = c : Hw2). Theorem LeInj {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c -:= obtain (w : Nat) (Hw : a + w = b), from (LeElim H), +:= Obtain (w : Nat) (Hw : a + w = b), from (LeElim H), LeIntro (calc a + c + w = a + (c + w) : Symm (PlusAssoc a c w) ... = a + (w + c) : { PlusComm c w } ... = a + w + c : PlusAssoc a w c ... = b + c : { Hw }). Theorem LeAntiSymm {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b -:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (LeElim H1), - obtain (w2 : Nat) (Hw2 : b + w2 = a), from (LeElim H2), +:= Obtain (w1 : Nat) (Hw1 : a + w1 = b), from (LeElim H1), + Obtain (w2 : Nat) (Hw2 : b + w2 = a), from (LeElim H2), let L1 : w1 + w2 = 0 := PlusInj (calc a + (w1 + w2) = a + w1 + w2 : { PlusAssoc a w1 w2 } ... = b + w2 : { Hw1 } diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 8ae590ae97..72f0d681d4 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -106,16 +106,16 @@ Theorem Absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false Theorem EqMP {a b : Bool} (H1 : a == b) (H2 : a) : b := Subst H2 H1. -(* assume is a 'macro' that expands into a Discharge *) +(* Assume is a 'macro' that expands into a Discharge *) Theorem ImpTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b ⇒ c) : a ⇒ c -:= assume Ha, MP H2 (MP H1 Ha). +:= Assume Ha, MP H2 (MP H1 Ha). Theorem ImpEqTrans {a b c : Bool} (H1 : a ⇒ b) (H2 : b == c) : a ⇒ c -:= assume Ha, EqMP H2 (MP H1 Ha). +:= Assume Ha, EqMP H2 (MP H1 Ha). Theorem EqImpTrans {a b c : Bool} (H1 : a == b) (H2 : b ⇒ c) : a ⇒ c -:= assume Ha, MP H2 (EqMP H1 Ha). +:= Assume Ha, MP H2 (EqMP H1 Ha). Theorem DoubleNeg (a : Bool) : (¬ ¬ a) == a := Case (λ x, (¬ ¬ x) == x) Trivial Trivial a. @@ -124,10 +124,10 @@ Theorem DoubleNegElim {a : Bool} (H : ¬ ¬ a) : a := EqMP (DoubleNeg a) H. Theorem MT {a b : Bool} (H1 : a ⇒ b) (H2 : ¬ b) : ¬ a -:= assume H : a, Absurd (MP H1 H) H2. +:= Assume H : a, Absurd (MP H1 H) H2. Theorem Contrapos {a b : Bool} (H : a ⇒ b) : ¬ b ⇒ ¬ a -:= assume H1 : ¬ b, MT H H1. +:= Assume H1 : ¬ b, MT H H1. Theorem AbsurdElim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b := FalseElim b (Absurd H1 H2). @@ -135,17 +135,17 @@ Theorem AbsurdElim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b Theorem NotImp1 {a b : Bool} (H : ¬ (a ⇒ b)) : a := DoubleNegElim (show ¬ ¬ a, - assume H1 : ¬ a, Absurd (show a ⇒ b, assume H2 : a, AbsurdElim b H2 H1) + Assume H1 : ¬ a, Absurd (show a ⇒ b, Assume H2 : a, AbsurdElim b H2 H1) (show ¬ (a ⇒ b), H)). Theorem NotImp2 {a b : Bool} (H : ¬ (a ⇒ b)) : ¬ b -:= assume H1 : b, Absurd (show a ⇒ b, assume H2 : a, H1) +:= Assume H1 : b, Absurd (show a ⇒ b, Assume H2 : a, H1) (show ¬ (a ⇒ b), H). (* Remark: conjunction is defined as ¬ (a ⇒ ¬ b) in Lean *) Theorem Conj {a b : Bool} (H1 : a) (H2 : b) : a ∧ b -:= assume H : a ⇒ ¬ b, Absurd H2 (MP H H1). +:= Assume H : a ⇒ ¬ b, Absurd H2 (MP H H1). Theorem Conjunct1 {a b : Bool} (H : a ∧ b) : a := NotImp1 H. @@ -156,20 +156,20 @@ Theorem Conjunct2 {a b : Bool} (H : a ∧ b) : b (* Remark: disjunction is defined as ¬ a ⇒ b in Lean *) Theorem Disj1 {a : Bool} (H : a) (b : Bool) : a ∨ b -:= assume H1 : ¬ a, AbsurdElim b H H1. +:= Assume H1 : ¬ a, AbsurdElim b H H1. Theorem Disj2 {b : Bool} (a : Bool) (H : b) : a ∨ b -:= assume H1 : ¬ a, H. +:= Assume H1 : ¬ a, H. Theorem ArrowToImplies {a b : Bool} (H : a → b) : a ⇒ b -:= assume H1 : a, H H1. +:= Assume H1 : a, H H1. Theorem Resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b := MP H1 H2. Theorem DisjCases {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c := DoubleNegElim - (assume H : ¬ c, + (Assume H : ¬ c, Absurd (show c, H3 (show b, Resolve1 H1 (show ¬ a, (MT (ArrowToImplies H2) H)))) H) @@ -180,7 +180,7 @@ Theorem Symm {A : TypeU} {a b : A} (H : a == b) : b == a := Subst (Refl a) H. Theorem NeSymm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a -:= assume H1 : b = a, MP H (Symm H1). +:= Assume H1 : b = a, MP H (Symm H1). Theorem EqNeTrans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c := Subst H2 (Symm H1). @@ -195,8 +195,8 @@ Theorem EqTElim {a : Bool} (H : a == true) : a := EqMP (Symm H) Trivial. Theorem EqTIntro {a : Bool} (H : a) : a == true -:= ImpAntisym (assume H1 : a, Trivial) - (assume H2 : true, H). +:= ImpAntisym (Assume H1 : a, Trivial) + (Assume H2 : true, H). Theorem Congr1 {A : TypeU} {B : A → TypeU} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a := SubstP (fun h : (Π x : A, B x), f a == h a) (Refl (f a)) H. @@ -229,11 +229,11 @@ Theorem ForallIntro {A : TypeU} {P : A → Bool} (H : Π x : A, P x) : Forall A Theorem ExistsElim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : Π (a : A) (H : P a), B) : B := Refute (λ R : ¬ B, - Absurd (ForallIntro (λ a : A, MT (assume H : P a, H2 a H) R)) + Absurd (ForallIntro (λ a : A, MT (Assume H : P a, H2 a H) R)) H1). Theorem ExistsIntro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P -:= assume H1 : (∀ x : A, ¬ P x), +:= Assume H1 : (∀ x : A, ¬ P x), Absurd H (ForallElim H1 a). (* @@ -250,26 +250,26 @@ SetOpaque and true. SetOpaque forall true. Theorem OrComm (a b : Bool) : (a ∨ b) == (b ∨ a) -:= ImpAntisym (assume H, DisjCases H (λ H1, Disj2 b H1) (λ H2, Disj1 H2 a)) - (assume H, DisjCases H (λ H1, Disj2 a H1) (λ H2, Disj1 H2 b)). +:= ImpAntisym (Assume H, DisjCases H (λ H1, Disj2 b H1) (λ H2, Disj1 H2 a)) + (Assume H, DisjCases H (λ H1, Disj2 a H1) (λ H2, Disj1 H2 b)). Theorem OrAssoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c)) -:= ImpAntisym (assume H : (a ∨ b) ∨ c, +:= ImpAntisym (Assume H : (a ∨ b) ∨ c, DisjCases H (λ H1 : a ∨ b, DisjCases H1 (λ Ha : a, Disj1 Ha (b ∨ c)) (λ Hb : b, Disj2 a (Disj1 Hb c))) (λ Hc : c, Disj2 a (Disj2 b Hc))) - (assume H : a ∨ (b ∨ c), + (Assume H : a ∨ (b ∨ c), DisjCases H (λ Ha : a, (Disj1 (Disj1 Ha b) c)) (λ H1 : b ∨ c, DisjCases H1 (λ Hb : b, Disj1 (Disj2 a Hb) c) (λ Hc : c, Disj2 (a ∨ b) Hc))). Theorem OrId (a : Bool) : (a ∨ a) == a -:= ImpAntisym (assume H, DisjCases H (λ H1, H1) (λ H2, H2)) - (assume H, Disj1 H a). +:= ImpAntisym (Assume H, DisjCases H (λ H1, H1) (λ H2, H2)) + (Assume H, Disj1 H a). Theorem OrRhsFalse (a : Bool) : (a ∨ false) == a -:= ImpAntisym (assume H, DisjCases H (λ H1, H1) (λ H2, FalseElim a H2)) - (assume H, Disj1 H false). +:= ImpAntisym (Assume H, DisjCases H (λ H1, H1) (λ H2, FalseElim a H2)) + (Assume H, Disj1 H false). Theorem OrLhsFalse (a : Bool) : (false ∨ a) == a := Trans (OrComm false a) (OrRhsFalse a). @@ -284,34 +284,34 @@ Theorem OrAnotA (a : Bool) : (a ∨ ¬ a) == true := EqTIntro (EM a). Theorem AndComm (a b : Bool) : (a ∧ b) == (b ∧ a) -:= ImpAntisym (assume H, Conj (Conjunct2 H) (Conjunct1 H)) - (assume H, Conj (Conjunct2 H) (Conjunct1 H)). +:= ImpAntisym (Assume H, Conj (Conjunct2 H) (Conjunct1 H)) + (Assume H, Conj (Conjunct2 H) (Conjunct1 H)). Theorem AndId (a : Bool) : (a ∧ a) == a -:= ImpAntisym (assume H, Conjunct1 H) - (assume H, Conj H H). +:= ImpAntisym (Assume H, Conjunct1 H) + (Assume H, Conj H H). Theorem AndAssoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c)) -:= ImpAntisym (assume H, Conj (Conjunct1 (Conjunct1 H)) (Conj (Conjunct2 (Conjunct1 H)) (Conjunct2 H))) - (assume H, Conj (Conj (Conjunct1 H) (Conjunct1 (Conjunct2 H))) (Conjunct2 (Conjunct2 H))). +:= ImpAntisym (Assume H, Conj (Conjunct1 (Conjunct1 H)) (Conj (Conjunct2 (Conjunct1 H)) (Conjunct2 H))) + (Assume H, Conj (Conj (Conjunct1 H) (Conjunct1 (Conjunct2 H))) (Conjunct2 (Conjunct2 H))). Theorem AndRhsTrue (a : Bool) : (a ∧ true) == a -:= ImpAntisym (assume H : a ∧ true, Conjunct1 H) - (assume H : a, Conj H Trivial). +:= ImpAntisym (Assume H : a ∧ true, Conjunct1 H) + (Assume H : a, Conj H Trivial). Theorem AndLhsTrue (a : Bool) : (true ∧ a) == a := Trans (AndComm true a) (AndRhsTrue a). Theorem AndRhsFalse (a : Bool) : (a ∧ false) == false -:= ImpAntisym (assume H, Conjunct2 H) - (assume H, FalseElim (a ∧ false) H). +:= ImpAntisym (Assume H, Conjunct2 H) + (Assume H, FalseElim (a ∧ false) H). Theorem AndLhsFalse (a : Bool) : (false ∧ a) == false := Trans (AndComm false a) (AndRhsFalse a). Theorem AndAnotA (a : Bool) : (a ∧ ¬ a) == false -:= ImpAntisym (assume H, Absurd (Conjunct1 H) (Conjunct2 H)) - (assume H, FalseElim (a ∧ ¬ a) H). +:= ImpAntisym (Assume H, Absurd (Conjunct1 H) (Conjunct2 H)) + (Assume H, FalseElim (a ∧ ¬ a) H). Theorem NotTrue : (¬ true) == false := Trivial @@ -397,7 +397,7 @@ Theorem UnfoldExists2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : ExistsIntro w (Conjunct2 Hw))). Theorem UnfoldExists {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x)) -:= ImpAntisym (assume H : (∃ x : A, P x), UnfoldExists1 a H) - (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), UnfoldExists2 a H). +:= ImpAntisym (Assume H : (∃ x : A, P x), UnfoldExists1 a H) + (Assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), UnfoldExists2 a H). SetOpaque exists true. diff --git a/src/builtin/macros.lua b/src/builtin/macros.lua index 3e9c1e09ff..b0d1ed5c62 100644 --- a/src/builtin/macros.lua +++ b/src/builtin/macros.lua @@ -83,11 +83,11 @@ function nary_macro(name, f, farity) end) end -binder_macro("for", Const("ForallIntro"), 3, 1, 3) -binder_macro("assume", Const("Discharge"), 3, 1, 3) -nary_macro("instantiate", Const("ForallElim"), 4) -nary_macro("mp", Const("MP"), 4) -nary_macro("subst", Const("Subst"), 6) +binder_macro("For", Const("ForallIntro"), 3, 1, 3) +binder_macro("Assume", Const("Discharge"), 3, 1, 3) +nary_macro("Instantiate", Const("ForallElim"), 4) +nary_macro("MP'", Const("MP"), 4) +nary_macro("Subst'", Const("Subst"), 6) -- ExistsElim syntax-sugar -- Example: @@ -103,7 +103,7 @@ nary_macro("subst", Const("Subst"), 6) -- ExistsElim Haux -- (fun (b : Na) (H : P a b), -- show false, Absurd H (instantiate Ax2 a b) -macro("obtain", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Id, macro_arg.Expr, macro_arg.Comma, macro_arg.Expr }, +macro("Obtain", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Id, macro_arg.Expr, macro_arg.Comma, macro_arg.Expr }, function (env, bindings, fromid, exPr, body) local n = #bindings if n < 2 then diff --git a/tests/lean/subst3.lean b/tests/lean/subst3.lean index 42de003a3b..0745cb99aa 100644 --- a/tests/lean/subst3.lean +++ b/tests/lean/subst3.lean @@ -1,7 +1,7 @@ (** import("macros.lua") **) Theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x) => x = y => x = z => p (f y z) := - for x y z, assume (H1 : p (f x x)) (H2 : x = y) (H3 : x = z), - subst H1 H2 H3. + For x y z, Assume (H1 : p (f x x)) (H2 : x = y) (H3 : x = z), + Subst' H1 H2 H3. Show Environment 1. \ No newline at end of file