Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r1599 r1882  
    5353
    5454(* should be proved in nat.ma, but it's not! *)
     55(* Paolo: there is eqb_elim which does something very similar *)
    5556lemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
    5657#n elim n;
     
    135136 ]
    136137qed.
     138
     139lemma associative_orb : associative ? orb.
     140*** // qed.
     141
     142lemma commutative_orb : commutative ? orb.
     143** // qed.
     144
     145lemma associative_andb : associative ? andb.
     146*** // qed.
     147
     148lemma commutative_andb : commutative ? andb.
     149** // qed.
     150
     151
     152lemma notb_false : ∀b.(¬b) = false → b = true.
     153* [#_ % | normalize #EQ destruct]
     154qed.
     155
     156lemma notb_true : ∀b.(¬b) = true → b = false.
     157* [normalize #EQ destruct | #_ %]
     158qed.
     159
     160
     161
     162notation > "Σ 〈 ident x : tyx, ident y : tyy 〉 . P" with precedence 20 for
     163  @{'sigma (λ${fresh p}.
     164    match ${fresh p} with [mk_Prod (${ident x} : $tyx) (${ident y} : $tyy) ⇒ $P])}.
     165notation > "Σ 〈 ident x, ident y 〉 . P" with precedence 20 for
     166  @{'sigma (λ${fresh p}.
     167    match ${fresh p} with [mk_Prod ${ident x} ${ident y} ⇒ $P])}.
     168notation > "Σ 〈 ident x : tyx, ident y : tyy, ident z : tyz 〉 . P" with precedence 20 for
     169  @{'sigma (λ${fresh p1}.
     170    match ${fresh p1} with [mk_Prod ${fresh p2} (${ident z} : $tyz) ⇒
     171      match ${fresh p2} with [mk_Prod (${ident x} : $tyx) (${ident y} : $tyy) ⇒ $P]])}.
     172notation > "Σ 〈 ident x , ident y , ident z 〉 . P" with precedence 20 for
     173  @{'sigma (λ${fresh p1}.
     174    match ${fresh p1} with [mk_Prod ${fresh p2} ${ident z} ⇒
     175      match ${fresh p2} with [mk_Prod ${ident x} ${ident y} ⇒ $P]])}.
     176
Note: See TracChangeset for help on using the changeset viewer.