Changeset 992 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 17, 2011, 6:05:05 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r991 r992 78 78 qed. 79 79 80 axiom vector_associative_append: 81 ∀A: Type[0]. 82 ∀n, m, o: nat. 83 ∀v: Vector A n. 84 ∀q: Vector A m. 85 ∀r: Vector A o. 86 ((v @@ q) @@ r) 87 ≃ 88 (v @@ (q @@ r)). 89 80 lemma super_rewrite2: 81 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m. 82 ∀P: ∀m. Vector A m → Prop. 83 n=m → v1 ≃ v2 → P n v1 → P m v2. 84 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ // 85 qed. 86 90 87 lemma vector_cons_append: 91 88 ∀A: Type[0]. … … 103 100 qed. 104 101 105 lemma super_rewrite2: 106 ∀A:Type[0].∀n,m.∀v1: Vector A n.∀v2: Vector A m. 107 ∀P: ∀m. Vector A m → Prop. 108 n=m → v1 ≃ v2 → P n v1 → P m v2. 109 #A #n #m #v1 #v2 #P #EQ <EQ in v2; #V #JMEQ >JMEQ // 102 lemma vector_cons_append2: 103 ∀A: Type[0]. 104 ∀n, m: nat. 105 ∀v: Vector A n. 106 ∀q: Vector A m. 107 ∀hd: A. 108 hd:::(v@@q) = (hd:::v)@@q. 109 #A #n #m #v #q 110 elim v 111 [ #hd % 112 | #n' #hd' #tl' #ih #hd' <ih % 113 ] 114 qed. 115 116 lemma jmeq_cons_vector_monotone: 117 ∀A: Type[0]. 118 ∀m, n: nat. 119 ∀v: Vector A m. 120 ∀q: Vector A n. 121 ∀prf: m = n. 122 ∀hd: A. 123 v ≃ q → hd:::v ≃ hd:::q. 124 #A #m #n #v #q #prf #hd #E 125 @(super_rewrite2 A … E) 126 [ assumption | @jmrefl ] 127 qed. 128 129 lemma vector_associative_append: 130 ∀A: Type[0]. 131 ∀n, m, o: nat. 132 ∀v: Vector A n. 133 ∀q: Vector A m. 134 ∀r: Vector A o. 135 ((v @@ q) @@ r) 136 ≃ 137 (v @@ (q @@ r)). 138 #A #n #m #o #v #q #r 139 elim v 140 [ % 141 | #n' #hd #tl #ih 142 <(vector_cons_append2 A … hd) 143 @jmeq_cons_vector_monotone 144 // 145 ] 110 146 qed. 111 147
Note: See TracChangeset
for help on using the changeset viewer.