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

chore(tests/lean/run/matrix): simplify same_dim_irrel proof

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-25 09:27:19 -07:00
parent 60d5e87a66
commit 42a8fb5965
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
tests/lean/run/matrix.lean
View file

@ -5,8 +5,7 @@ variable same_dim {A : Type} : matrix A → matrix A → Prop
variable add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A variable add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A
theorem same_dim_irrel {A : Type} {m1 m2 : matrix A} {H1 H2 : same_dim m1 m2} : @add A m1 m2 H1 = @add A m1 m2 H2 := theorem same_dim_irrel {A : Type} {m1 m2 : matrix A} {H1 H2 : same_dim m1 m2} : @add A m1 m2 H1 = @add A m1 m2 H2 :=
have eq : H1 = H2, from rfl, rfl
subst eq rfl
theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : same_dim m1' m2' := theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : same_dim m1' m2' :=
subst H1 (subst H2 H) subst H1 (subst H2 H)