# Changeset 1972 for src/ASM

Ignore:
Timestamp:
May 21, 2012, 10:33:26 AM (8 years ago)
Message:

Simple lemma with strangely complex proof complete.

File:
1 edited

Unmodified
Added
Removed
• ## src/ASM/AssemblyProof.ma

 r1966 qed. lemma destruct_bug_fix: lemma destruct_bug_fix_1: ∀n: nat. S n = 0 → False. #n #absurd destruct(absurd) qed. lemma destruct_bug_fix_2: ∀m, n: nat. S m = S n → m = n. #m #n #refl destruct % qed. @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]])) [1: #absurd @⊥ -b @(destruct_bug_fix 2) #absurd @⊥ -b @(destruct_bug_fix_1 2) >absurd % |2: cut (n = 2) [1: @destruct_bug_fix_2 >size_refl % |2: #n_refl >n_refl in tl; cases daemon #n_refl >n_refl in tl; #V @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]])) [1: #absurd @⊥ -V @(destruct_bug_fix_1 1) >absurd % |2: #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'} cut (n' = 1) [1: @destruct_bug_fix_2 >size_refl' % |2: #n_refl' >n_refl' in tl'; #V' @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]])) [1: #absurd @⊥ -V' @(destruct_bug_fix_1 0) >absurd % |2: #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''} cut (n'' = 0) [1: @destruct_bug_fix_2 >size_refl'' % |2: #n_refl'' >n_refl'' in tl''; #tl''' >(Vector_O … tl''') % ] ] ] ] ] ] cases daemon qed.
Note: See TracChangeset for help on using the changeset viewer.