Changeset 1977


Ignore:
Timestamp:
May 22, 2012, 12:05:22 AM (5 years ago)
Author:
sacerdot
Message:

Unblocked: let ... as hides two different terms, one that uses Leibniz
and one that uses JM. The latter is required here. The lemma to be proved
is a nightmare, but it should be provable.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r1975 r1977  
    134134qed.
    135135
    136 lemma pair_as_replace:
    137  ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. 〈a, b〉 = c' → T. ∀EQc: c'= c.
    138   c ≃ 〈a,b〉 →
    139   P (let 〈a, b〉 as H ≝ c in t a b ?) → P (let 〈a',b'〉 as H ≝ c' in t a' b' H).
     136lemma jmpair_as_replace:
     137 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c.
     138  ∀EQ:c ≃ 〈a,b〉.
     139  P (t a b ?) → P ((let 〈a',b'〉 (*as H*) ≝ c' in λH. t a' b' H) (refl_jmeq ? c')).
    140140  [2:
    141     >EQc assumption
     141    >EQc @EQ
    142142  |1:
    143     #A #B #T #P #a #b * #x #y * #x' #y' #t #H1 #H2 destruct //
    144   ]
     143    #A #B #T #P #a #b
     144    #c #c' #t #EQc >EQc in t; -c' #f #EQ normalize lapply f lapply EQ -EQ -f cases c
     145    cases daemon (* CSC: extremely difficult to prove...
     146    normalize #a' #b' @(pose … 〈a,b〉) #H #f
     147    @(pose … 〈a,b〉)
     148     @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) H)) ?? H)
     149    check(E ????? H)
     150    cut (a=a' ∧ b=b')
     151    [ destruct /2/
     152    | * #EQa #EQb >EQa in H; >EQb #H check (E ????? H)
     153     #H cut (a=a') [2: #Eqa >Eqa in H; #H
     154   
     155   
     156     * #x #y * #x' #y' #t #H1 #H2 cases H1 in H2; normalize
     157    #X -H1 destruct(X) destruct //
     158  ]*)
    145159qed.
    146160
     
    644658  (* XXX: work on sigma commutation *)
    645659  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
    646   (* XXX: work on ticks (of all kinds) *)
    647   >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
    648660  (* XXX: work on both sides *)
    649661  [1,2,3,4,5:
     
    655667  ]
    656668  <EQaddr normalize nodelta #irrelevant
    657   [1:
    658     @(pair_as_replace ??? (λx. pi1 ?? x = ?) ???? (λx. λy. λ_. half_add ???) ? p)
    659  
     669  try @(jmpair_as_replace ?????????? p)
     670  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
     671  normalize nodelta
     672  (* XXX: work on ticks (of all kinds) *)
     673  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
    660674  (* XXX: removes status 's' *)
    661675  normalize nodelta >EQs -s -ticks
    662676  whd in ⊢ (??%%);
    663677  (* XXX: simplify the left hand side *)
    664 
     678  cases daemon
    665679  (* XXX: work on both sides *)
    666680|1,2,3,9,51,53,54,55: (* ADD, ADDC, SUBB, DEC, POP, XCHD, RET, RETI  *)
Note: See TracChangeset for help on using the changeset viewer.