# Changeset 1599 for src/ASM/Util.ma

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

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

File:
1 edited

### Legend:

Unmodified
 r1598 include "basics/list.ma". include "basics/lists/list.ma". include "basics/types.ma". include "arithmetics/nat.ma". include "utilities/pair.ma". include "ASM/JMCoercions.ma". notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ match $e in bool with [ true ⇒$t | false ⇒ $f] }. 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 for @{ match$e with [ true ⇒ $t | false ⇒$f]  }. let rec fold_left_i_aux (A: Type[0]) (B: Type[0]) (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝ | S o ⇒ f (iterate A f a o) ]. (* Yeah, I probably ought to do something more general... *) notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)" with precedence 90 for @{ 'triple $a$b $c}. interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z). notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)" with precedence 90 for @{ 'quadruple$a $b$c $d}. interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)). notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)" with precedence 10 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 ] ] ] }. notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)" with precedence 10 for @{ match$t with [ pair ${fresh xy}${ident z} ⇒ match ${fresh xy} with [ pair${ident x} ${ident y} ⇒$s ] ] }. notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)" with precedence 10 for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒$s ] }. axiom pair_elim': ∀A,B,C: Type[0]. ∀T: A → B → C. ∀p. ∀P: A×B → C → Prop. (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) → P p (let 〈lft, rgt〉 ≝ p in T lft rgt). axiom pair_elim'': ∀A,B,C,C': Type[0]. ∀T: A → B → C. ∀T': A → B → C'. ∀p. ∀P: A×B → C → C' → Prop. (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) → P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt). lemma pair_destruct_1: ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c. #A #B #a #b *; /2/ qed. lemma pair_destruct_2: ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c. #A #B #a #b *; /2/ qed. let rec exclusive_disjunction (b: bool) (c: bool) on b ≝ match b with [ true ⇒ match c with [ false ⇒ true | true ⇒ false ] | false ⇒ match c with [ false ⇒ false | true ⇒ true ] ]. (* dpm: conflicts with library definitions interpretation "Nat less than" 'lt m n = (ltb m n). interpretation "Nat greater than" 'gt m n = (gtb m n). interpretation "Nat greater than eq" 'geq m n = (geb m n). *) let rec division_aux (m: nat) (n : nat) (p: nat) ≝ elim b normalize [ /2/ [ /2 by conj/ | # K destruct