michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(*): name convention, proof construnction functions/macros start with upper-case

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-03 18:11:01 -08:00
parent 9eb4dc4a81
commit fbe0bccf51
7 changed files with 78 additions and 78 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/lean/ex2.lean
View file

@ -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.

6
examples/lean/ex3.lean
View file

@ -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)).

28
examples/lean/set.lean
View file

@ -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))

22
src/builtin/Nat.lean
View file

@ -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 }

80
src/builtin/kernel.lean
View file

@ -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.

12
src/builtin/macros.lua
View file

@ -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

4
tests/lean/subst3.lean
View file

@ -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.