max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add test

Browse source
This commit is contained in:
Mario Carneiro 2022-09-21 23:36:09 -04:00 • committed by Leonardo de Moura
parent fa13d7321f
commit 121b18f40a
1 changed files with 24 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

53
tests/lean/run/generalize.lean
View file

@ -1,35 +1,30 @@
theorem tst0 (x : Nat) : x + 0 = x + 0 :=
by {
generalize x + 0 = y;
exact (Eq.refl y)
}
example (x : Nat) : x + 0 = x + 0 := by
generalize x + 0 = y
rfl
theorem tst1 (x : Nat) : x + 0 = x + 0 :=
by {
generalize h : x + 0 = y;
exact (Eq.refl y)
}
example (x : Nat) : x + 0 = x + 0 := by
generalize h : x + 0 = y
rfl
theorem tst2 (x y w : Nat) (h : y = w) : (x + x) + w = (x + x) + y :=
by {
generalize h' : x + x = z;
subst y;
exact Eq.refl $ z + w
}
example (x y w : Nat) (h : y = w) : (x + x) + w = (x + x) + y := by
generalize h' : x + x = z
subst y
rfl
theorem tst3 (x y w : Nat) (h : x + x = y) : (x + x) + (x+x) = (x + x) + y :=
by {
generalize h' : x + x = z;
subst z;
subst y;
exact rfl
}
example (x y w : Nat) (h : x + x = y) : (x + x) + (x+x) = (x + x) + y := by
generalize h' : x + x = z
subst z
subst y
rfl
theorem tst4 (x y w : Nat) (h : y = w) : (x + x) + w = (x + x) + y :=
by {
generalize h' : x + y = z; -- just add equality
subst h;
exact rfl
}
example (x y w : Nat) (h : y = w) : (x + x) + w = (x + x) + y := by
generalize h' : x + y = z -- just add equality
subst h
rfl
example (x y w : Nat) (h : y = w) (H : (x + x) + w = (x + x) + y) :
(x + x) + w = (x + x) + y := by
generalize h' : x + x = z at H
exact H