Changeset 1979


Ignore:
Timestamp:
May 22, 2012, 12:57:17 AM (6 years ago)
Author:
sacerdot
Message:

Very very very tricky lemma closed. A dreadful mix of JM equality elimination
and lack of eta-conversion in the logic.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r1978 r1979  
    142142  |1:
    143143    #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   ]*)
     144    #c #c' #t #EQc >EQc in t; -c' normalize #f #EQ
     145    letin eta ≝ (? : ∀ab:A × B.∀P:A × B → Type[0]. P ab → P 〈\fst ab,\snd ab〉) [2: * // ]
     146    change with (eta 〈a,b〉 (λab.c ≃ ab) EQ) in match EQ;
     147    @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) ?) → ?) ?? EQ) normalize -eta
     148    -EQ cases c in f; normalize //
     149  ]
    159150qed.
    160151
Note: See TracChangeset for help on using the changeset viewer.