# Changeset 3530

Ignore:
Timestamp:
Mar 13, 2015, 5:03:17 PM (5 years ago)
Message:

prova in corso lemma che il predicato sul tipo expr corrisponde all'uguaglianza

File:
1 edited

Unmodified
Removed
• ## LTS/imp.ma

 r3529 | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q] ]. axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m. axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m. lemma neqb_sym:∀n.neqb n n=true. #n elim n [%|#n' normalize * %]qed. definition cond_i:Type[0]≝condition. |Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]]. lemma expr_eq_aux:∀e:expr.expr_eq e e=true. #e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * @neqb_sym |3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed. lemma expr_eq_equality_one:∀e1,e2:expr.expr_eq e1 e2=true → e1=e2. #e1 elim e1 [1,2: #v1 * normalize [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) #A destruct >(A H) % |3,4,7,8: #e #f #ABS destruct] |3,4: #e * [1,2,5: #v2 #H #K #f #T normalize in T; [1,2,5,6: #v2 #H /10 by _/ lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔e1=e2. #e1 #e2 elim e1 elim e2 normalize [#v #v' % #H elim v elim v' normalize in H; [%|#v2 #H' destruct #e1 elim e1 [ #v1 * [ #v2 normalize % #H cases (neqb_true_to_eq v1 v2) #H1 #H2 >H1 // destruct /2/ | #c normalize % #H destruct |*: cases daemon ] | | #e1 #e2 #IH1 #IH2 * [3: #f1 #f2 normalize % [ inversion (expr_eq e1 f1) normalize #H1 #H2 [2: destruct ] cases (IH1 f1) cases (IH2 f2) /4 by eq_f2, sym_eq/ | #H destruct cases (IH1 f1) cases (IH2 f2) #H1 #H2 #H3 #H4 >H4/2 by / #e1 #e2 elim e1 elim e2 [#v #v' % elim v elim v' [#_ %|#v2 #IH #H normalize in H; destruct |#v2 #IH #H normalize in H; destruct|#v2 #H #v3 #K #T normalize in T; lapply(neqb_true_to_eq v2 v3) * #A1 >(A1 T) #_ %|#_ %|#v2 #H #ABS destruct|#v2 #H #ABS destruct|#v1 #H #v2 #K #J destruct normalize lapply(neqb_true_to_eq v2 v2) * #_ #A >A %] |#n #v % #H normalize in H; destruct|#f1 #f2 #A #B #v % #ABS normalize in ABS; destruct |#f1 #f2 #A #B #v % #ABS normalize in ABS; destruct |#v #n % normalize #ABS destruct|#n1 #n2 % normalize #H destruct [lapply(neqb_true_to_eq n2 n1) * #A >(A H) #_ % | lapply(neqb_true_to_eq n1 n1) * #_ * %] (*end Var *) |#f1 #f2 #_ #_ #n % normalize #ABS destruct |#f1 #f2 #_ #_ #n % normalize #ABS destruct |#v #f1 #f2 #_ #_ % normalize #ABS destruct |#n #f1 #f2 #_ #_ % normalize #ABS destruct (* end Const*) |#f1 #f2 #H1 #H2 #e1' #e2' #IH1 #IH2 % [2:#D destruct(D) normalize elim f1 [#v normalize lapply(neqb_true_to_eq v v) * #_ #A >(A …) [2:%] normalize elim f2 [#v' normalize lapply(neqb_true_to_eq v' v') * #_ #B >(B …) [2:%] normalize % |#v' normalize lapply(neqb_true_to_eq v' v') * #_ #B >(B …) [2:%] normalize % |#e #f #IHe #IHf normalize >IHe >IHf normalize % |#e #f #IHe #IHf normalize >IHe >IHf normalize %] |#n normalize lapply(neqb_true_to_eq n n) * #_ #A >(A \dots) [2:%] normalize elim f2 [#v' normalize lapply(neqb_true_to_eq v' v') * #_ #B >(B …) [2:%] normalize % |#v' normalize lapply(neqb_true_to_eq v' v') * #_ #B >(B …) [2:%] normalize % |#e #f #IHe #IHf normalize >IHe >IHf normalize % |#e #f #IHe #IHf normalize >IHe >IHf normalize %] |#e #f inversion(expr_eq e e) inversion(expr_eq f f) #Hff #Hee normalize >Hff >Hee normalize #H * [%|% |destruct|%] |#e #f inversion(expr_eq e e) inversion(expr_eq f f) #Hff #Hee normalize >Hff >Hee normalize #H * [%|% |destruct|%]] |-IH1 -IH2  #H normalize in H; inversion(expr_eq e1' f1) inversion(expr_eq e2' f2) #I2 #I1 (*[cut((e2'=f2)∧(e1'=f1)) [% [elim e2' elim f2 [#v #v'*) >I1 in H; normalize >I2 #B destruct ] (* incompleto *) |#f1 #f2 #_ #_ #e #e' #_ #_ % #H normalize in H; destruct |#v #f1 #f2 #_ #_ % #H normalize in H; destruct |#n #f1 #f2 #_ #_ % #H normalize in H; destruct |#f1 #f2 #_ #_ #e #e' #_ #_ % #H normalize in H; destruct |#f1 #f2 #_ #_ #e #e' #_ #_ % [2:* normalize inversion(expr_eq e e) inversion(expr_eq e' e') #He #He' >He >He' normalize [%| #IHf normalize * #H6 #H7 cut(v2=v3) [@H6 @C|#K >K %]|#_ %| #v2 #H #ABS destruct|#v2 #H #ABS destruct|#v2 #H #v3 #K #T >T normalize elim v3 [%|#v4 normalize * %]]|#v1 #v2 % normalize #ABS destruct|#f1 #f2 #H1 #H2 #v % normalize #K destruct|#f1 #f2 #H1 #H2 #v % normalize #K destruct| #v #n % normalize #ABS destruct|#n1 #n2 % normalize #H [2: destruct elim n1 normalize [%|#n * %]| lapply (neqb_true_to_eq n2 n1) #A elim A * [#H22 %|@H]]|#f1 #f2 #H #K #n % normalize #ABS destruct|#f1 #f2 #H #K #n % normalize #ABS destruct |#v #f1 #f2 #H1 #H2 % normalize #ABS destruct|#n #f1 #f2 #H1 #H2 % normalize #ABS destruct |#f1 #f2 #_ #_ #ee1 #ee2 #_ #_ % [2:* normalize cases ee1 [#v normalize cases v normalize [cases ee2 [#v' normalize lapply(neqb_true_to_eq v' v') * #_ * % |#v' normalize lapply(neqb_true_to_eq v' v') * #_ * % |#ff1 #ff2 inversion(expr_eq ee1 f1) [#H1 normalize #H2 elim ee1 elim f1 elim ee2 elim f2 [#H559 #H560 #H561 #H562 #H563 #K [cut((ee1=f1)∧(ee2=f2))[% normalize in K; lemma condition_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2. #c1 #c2 elim c1 elim c2 [#H1 #H2 #H3 #H4 % #H normalize in H;
Note: See TracChangeset for help on using the changeset viewer.