Changeset 1599 for src/ASM/Util.ma


Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (8 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1598 r1599  
    1 include "basics/list.ma".
     1include "basics/lists/list.ma".
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
    4 
    5 include "utilities/pair.ma".
    64include "ASM/JMCoercions.ma".
    75
     
    649647
    650648   
    651 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
    652  for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
    653 notation < "hvbox('if' \nbsp term 19 e \nbsp break 'then' \nbsp term 19 t \nbsp break 'else' \nbsp term 48 f \nbsp)" non associative with precedence 19
    654  for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
    655 
    656649let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
    657650                        (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
     
    684677    | S o ⇒ f (iterate A f a o)
    685678    ].
    686 
    687 (* Yeah, I probably ought to do something more general... *)
    688 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
    689 with precedence 90 for @{ 'triple $a $b $c}.
    690 interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z).
    691 
    692 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
    693 with precedence 90 for @{ 'quadruple $a $b $c $d}.
    694 interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)).
    695 
    696 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
    697  with precedence 10
    698 for @{ match $t with [ pair ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ pair ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }.
    699 
    700 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
    701  with precedence 10
    702 for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
    703 
    704 notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
    705  with precedence 10
    706 for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
    707 
    708 axiom pair_elim':
    709   ∀A,B,C: Type[0].
    710   ∀T: A → B → C.
    711   ∀p.
    712   ∀P: A×B → C → Prop.
    713     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
    714       P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
    715 
    716 axiom pair_elim'':
    717   ∀A,B,C,C': Type[0].
    718   ∀T: A → B → C.
    719   ∀T': A → B → C'.
    720   ∀p.
    721   ∀P: A×B → C → C' → Prop.
    722     (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
    723       P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
    724 
    725 lemma pair_destruct_1:
    726  ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
    727  #A #B #a #b *; /2/
    728 qed.
    729 
    730 lemma pair_destruct_2:
    731  ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
    732  #A #B #a #b *; /2/
    733 qed.
    734 
    735 
    736 let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
    737   match b with
    738     [ true ⇒
    739       match c with
    740         [ false ⇒ true
    741         | true ⇒ false
    742         ]
    743     | false ⇒
    744       match c with
    745         [ false ⇒ false
    746         | true ⇒ true
    747         ]
    748     ].
    749 
    750 (* dpm: conflicts with library definitions
    751 interpretation "Nat less than" 'lt m n = (ltb m n).
    752 interpretation "Nat greater than" 'gt m n = (gtb m n).
    753 interpretation "Nat greater than eq" 'geq m n = (geb m n).
    754 *)
    755679
    756680let rec division_aux (m: nat) (n : nat) (p: nat) ≝
     
    891815  elim b
    892816  normalize
    893   [ /2/
     817  [ /2 by conj/
    894818  | # K
    895819    destruct
Note: See TracChangeset for help on using the changeset viewer.