Changeset 1062 for src/ASM/FoldStuff.ma


Ignore:
Timestamp:
Jul 11, 2011, 2:09:03 PM (9 years ago)
Author:
mulligan
Message:

separated jmeq and coercions from foldstuff.ma in order to fix the ongoing mess in util.ma surrounding reduce_strong

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/FoldStuff.ma

    r1014 r1062  
    1 (* RUSSEL **)
    2 
    3 include "basics/jmeq.ma".
    4 include "basics/types.ma".
    5 include "basics/list.ma".
    6 
    7 notation > "hvbox(a break ≃ b)"
    8   non associative with precedence 45
    9 for @{ 'jmeq ? $a ? $b }.
    10 
    11 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
    12   non associative with precedence 45
    13 for @{ 'jmeq $t $a $u $b }.
    14 
    15 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
    16 
    17 lemma eq_to_jmeq:
    18   ∀A: Type[0].
    19   ∀x, y: A.
    20     x = y → x ≃ y.
    21   //
    22 qed.
    23 
    24 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
    25 definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
    26 
    27 coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
    28 coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
    29 
    30 (*axiom VOID: Type[0].
    31 axiom assert_false: VOID.
    32 definition bigbang: ∀A:Type[0].False → VOID → A.
    33  #A #abs cases abs
    34 qed.
    35 
    36 coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.*)
    37 
    38 lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
    39  #A #P #p cases p #w #q @q
    40 qed.
    41 
    42 lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
    43  #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
    44 qed.
    45 
    46 coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
    47 
    48 (* END RUSSELL **)
    49 
    501include "ASM/Util.ma".
     2include "ASM/JMCoercions.ma".
    513
    524let rec foldl_strong_internal
Note: See TracChangeset for help on using the changeset viewer.