From 6fe06927f3293bfce4a01a587abd9913e711da88 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 23 Sep 2009 15:04:02 +0000 Subject: [PATCH] ... --- .../matita/tests/ng_coercion_and_hints.ma | 52 +++++++++++ helm/software/matita/tests/ng_copy.ma | 31 +++++++ helm/software/matita/tests/ng_copy2.ma | 21 +++++ helm/software/matita/tests/reduction_new.ma | 11 +++ .../matita/tests/reduction_new_preamble.ma | 90 ++++++++++++++++++ helm/software/matita/tests/reduction_old.ma | 10 ++ .../matita/tests/reduction_old_preamble.ma | 92 +++++++++++++++++++ 7 files changed, 307 insertions(+) create mode 100644 helm/software/matita/tests/ng_coercion_and_hints.ma create mode 100644 helm/software/matita/tests/ng_copy.ma create mode 100644 helm/software/matita/tests/ng_copy2.ma create mode 100755 helm/software/matita/tests/reduction_new.ma create mode 100644 helm/software/matita/tests/reduction_new_preamble.ma create mode 100755 helm/software/matita/tests/reduction_old.ma create mode 100644 helm/software/matita/tests/reduction_old_preamble.ma diff --git a/helm/software/matita/tests/ng_coercion_and_hints.ma b/helm/software/matita/tests/ng_coercion_and_hints.ma new file mode 100644 index 000000000..3aafc359a --- /dev/null +++ b/helm/software/matita/tests/ng_coercion_and_hints.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ng_pts.ma". +ndefinition hint_declaration_Type0 ≝ λA:Type[0] .λa,b:A.a. +ndefinition hint_declaration_Type1 ≝ λA:Type[1].λa,b:A.a. +ndefinition hint_declaration_Type2 ≝ λa,b:Type[1].a. +ndefinition hint_declaration_CProp0 ≝ λA:CProp[0].λa,b:A.a. +ndefinition hint_declaration_CProp1 ≝ λA:CProp[1].λa,b:A.a. +ndefinition hint_declaration_CProp2 ≝ λa,b:CProp[1].a. + +notation > "≔ (list0 (ident x : T )sep ,) ⊢ term 19 Px ≡ term 19 Py" + with precedence 90 + for @{ ${ fold right @{'hint_decl $Px $Py} rec acc @{ ∀${ident x}:$T.$acc } } }. + +interpretation "hint_decl_Type2" 'hint_decl a b = (hint_declaration_Type2 a b). +interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b). +interpretation "hint_decl_Type1" 'hint_decl a b = (hint_declaration_Type1 ? a b). +interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a b). +interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b). +interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b). + +naxiom A : Type[0]. +naxiom B : Type[0]. + +ndefinition C ≝ B. +ndefinition D ≝ A. + +naxiom f : B → A. + +ncoercion pippo : ∀a:B. A ≝ f on _a : B to A. + +alias symbol "hint_decl" = "hint_decl_Type1". +unification hint 0 ≔ ⊢ C ≡ B. +unification hint 0 ≔ ⊢ A ≡ D. + +naxiom pippo : D → Prop. + +nlemma foo : ∀c:C. pippo c. + + diff --git a/helm/software/matita/tests/ng_copy.ma b/helm/software/matita/tests/ng_copy.ma new file mode 100644 index 000000000..4bd5f18d5 --- /dev/null +++ b/helm/software/matita/tests/ng_copy.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +universe constraint Type[0] < Type[1]. +universe constraint Type[1] < Type[2]. +universe constraint CProp[0] < CProp[1]. +universe constraint CProp[1] < CProp[2]. +universe constraint Type[0] ≤ CProp[0]. +universe constraint CProp[0] ≤ Type[0]. +universe constraint Type[1] ≤ CProp[1]. +universe constraint CProp[1] ≤ Type[1]. +universe constraint Type[2] ≤ CProp[2]. +universe constraint CProp[2] ≤ Type[2]. + +ninductive A : Type[1] ≝ Foo : Type[0] → A. +(* +ncopy B from cic:/matita/tests/ng_copy/A.ind with + cic:/matita/pts/Type1.univ ↦ cic:/matita/pts/Type2.univ. +ntheorem foo : A → cic:/matita/tests/ng_copy/B.ind(0). +*) \ No newline at end of file diff --git a/helm/software/matita/tests/ng_copy2.ma b/helm/software/matita/tests/ng_copy2.ma new file mode 100644 index 000000000..7e74845ee --- /dev/null +++ b/helm/software/matita/tests/ng_copy2.ma @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ng_copy.ma". + +ncopy cic:/matita/tests/ng_copy/ +suffix 1 +change cic:/matita/pts/Type1.univ with cic:/matita/pts/Type2.univ +change cic:/matita/pts/Type1.univ with cic:/matita/pts/Type2.univ +change cic:/matita/pts/Type1.univ with cic:/matita/pts/Type2.univ diff --git a/helm/software/matita/tests/reduction_new.ma b/helm/software/matita/tests/reduction_new.ma new file mode 100755 index 000000000..b47a750d9 --- /dev/null +++ b/helm/software/matita/tests/reduction_new.ma @@ -0,0 +1,11 @@ +include "reduction_new_preamble.ma". + +ndefinition test: + 〈〈x0,x0〉:〈x0,xF〉〉 = + ((succ_w16(succ_w16(succ_w16 + (succ_w16(succ_w16(succ_w16(succ_w16 + (succ_w16(succ_w16(succ_w16(succ_w16 + (succ_w16(succ_w16(succ_w16(succ_w16 + 〈〈x0,x0〉:〈x0,x0〉〉)))))))))))))))). +napply (refl_eq word16 〈〈x0,x0〉:〈x0,xF〉〉); +nqed. diff --git a/helm/software/matita/tests/reduction_new_preamble.ma b/helm/software/matita/tests/reduction_new_preamble.ma new file mode 100644 index 000000000..4998dd035 --- /dev/null +++ b/helm/software/matita/tests/reduction_new_preamble.ma @@ -0,0 +1,90 @@ + +universe constraint Type[0] < Type[1]. + +ninductive exadecim : Type ≝ + x0: exadecim +| x1: exadecim +| x2: exadecim +| x3: exadecim +| x4: exadecim +| x5: exadecim +| x6: exadecim +| x7: exadecim +| x8: exadecim +| x9: exadecim +| xA: exadecim +| xB: exadecim +| xC: exadecim +| xD: exadecim +| xE: exadecim +| xF: exadecim. + +ninductive bool : Type ≝ true :bool | false : bool . + +ndefinition eq_ex ≝ +λe1,e2:exadecim. + match e1 with + [ x0 ⇒ match e2 with [ x0 ⇒ true | _ ⇒ false ] + | x1 ⇒ match e2 with [ x1 ⇒ true | _ ⇒ false ] + | x2 ⇒ match e2 with [ x2 ⇒ true | _ ⇒ false ] + | x3 ⇒ match e2 with [ x3 ⇒ true | _ ⇒ false ] + | x4 ⇒ match e2 with [ x4 ⇒ true | _ ⇒ false ] + | x5 ⇒ match e2 with [ x5 ⇒ true | _ ⇒ false ] + | x6 ⇒ match e2 with [ x6 ⇒ true | _ ⇒ false ] + | x7 ⇒ match e2 with [ x7 ⇒ true | _ ⇒ false ] + | x8 ⇒ match e2 with [ x8 ⇒ true | _ ⇒ false ] + | x9 ⇒ match e2 with [ x9 ⇒ true | _ ⇒ false ] + | xA ⇒ match e2 with [ xA ⇒ true | _ ⇒ false ] + | xB ⇒ match e2 with [ xB ⇒ true | _ ⇒ false ] + | xC ⇒ match e2 with [ xC ⇒ true | _ ⇒ false ] + | xD ⇒ match e2 with [ xD ⇒ true | _ ⇒ false ] + | xE ⇒ match e2 with [ xE ⇒ true | _ ⇒ false ] + | xF ⇒ match e2 with [ xF ⇒ true | _ ⇒ false ] + ]. + +ndefinition succ_ex ≝ +λe:exadecim. + match e with + [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8 + | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]. + + +nrecord byte8 : Type ≝ + { + b8h: exadecim; + b8l: exadecim + }. + +notation "〈x,y〉" non associative with precedence 80 + for @{ 'mk_byte8 $x $y }. +interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y). + +ndefinition andb ≝ λa,b.match a with [ true ⇒ b | _ ⇒ false ]. + +ndefinition eq_b8 ≝ λb1,b2:byte8.andb (eq_ex (b8h b1) (b8h b2)) (eq_ex (b8l b1) (b8l b2)). +ndefinition succ_b8 ≝ +λb:byte8.match eq_ex (b8l b) xF with + [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b)) + | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ]. + +nrecord word16 : Type ≝ + { + w16h: byte8; + w16l: byte8 + }. + +(* \langle \rangle *) +notation "〈x:y〉" non associative with precedence 80 + for @{ 'mk_word16 $x $y }. +interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y). + +ndefinition succ_w16 ≝ +λw:word16. + match eq_b8 (w16l w) (mk_byte8 xF xF) with + [ true ⇒ mk_word16 (succ_b8 (w16h w)) (succ_b8 (w16l w)) + | false ⇒ mk_word16 (w16h w) (succ_b8 (w16l w)) ]. + +ninductive eq (A:Type) (a:A) : A → Prop ≝ refl_eq : eq A a a. + +interpretation "aa" 'eq t a b = (eq t a b). + diff --git a/helm/software/matita/tests/reduction_old.ma b/helm/software/matita/tests/reduction_old.ma new file mode 100755 index 000000000..b0596ae1d --- /dev/null +++ b/helm/software/matita/tests/reduction_old.ma @@ -0,0 +1,10 @@ +include "reduction_old_preamble.ma". +definition test: + 〈〈x0,x0〉:〈x0,xF〉〉 = + ((succ_w16(succ_w16(succ_w16 + (succ_w16(succ_w16(succ_w16(succ_w16 + (succ_w16(succ_w16(succ_w16(succ_w16 + (succ_w16(succ_w16(succ_w16(succ_w16 + 〈〈x0,x0〉:〈x0,x0〉〉)))))))))))))))). +apply (refl_eq word16 〈〈x0,x0〉:〈x0,xF〉〉); +qed. diff --git a/helm/software/matita/tests/reduction_old_preamble.ma b/helm/software/matita/tests/reduction_old_preamble.ma new file mode 100644 index 000000000..b0578bf28 --- /dev/null +++ b/helm/software/matita/tests/reduction_old_preamble.ma @@ -0,0 +1,92 @@ + +inductive exadecim : Type ≝ + x0: exadecim +| x1: exadecim +| x2: exadecim +| x3: exadecim +| x4: exadecim +| x5: exadecim +| x6: exadecim +| x7: exadecim +| x8: exadecim +| x9: exadecim +| xA: exadecim +| xB: exadecim +| xC: exadecim +| xD: exadecim +| xE: exadecim +| xF: exadecim. + +inductive bool : Type ≝ true :bool | false : bool . + +(* operatore = *) +definition eq_ex ≝ +λe1,e2:exadecim. + match e1 with + [ x0 ⇒ match e2 with [ x0 ⇒ true | _ ⇒ false ] + | x1 ⇒ match e2 with [ x1 ⇒ true | _ ⇒ false ] + | x2 ⇒ match e2 with [ x2 ⇒ true | _ ⇒ false ] + | x3 ⇒ match e2 with [ x3 ⇒ true | _ ⇒ false ] + | x4 ⇒ match e2 with [ x4 ⇒ true | _ ⇒ false ] + | x5 ⇒ match e2 with [ x5 ⇒ true | _ ⇒ false ] + | x6 ⇒ match e2 with [ x6 ⇒ true | _ ⇒ false ] + | x7 ⇒ match e2 with [ x7 ⇒ true | _ ⇒ false ] + | x8 ⇒ match e2 with [ x8 ⇒ true | _ ⇒ false ] + | x9 ⇒ match e2 with [ x9 ⇒ true | _ ⇒ false ] + | xA ⇒ match e2 with [ xA ⇒ true | _ ⇒ false ] + | xB ⇒ match e2 with [ xB ⇒ true | _ ⇒ false ] + | xC ⇒ match e2 with [ xC ⇒ true | _ ⇒ false ] + | xD ⇒ match e2 with [ xD ⇒ true | _ ⇒ false ] + | xE ⇒ match e2 with [ xE ⇒ true | _ ⇒ false ] + | xF ⇒ match e2 with [ xF ⇒ true | _ ⇒ false ] + ]. + +definition succ_ex ≝ +λe:exadecim. + match e with + [ x0 ⇒ x1 | x1 ⇒ x2 | x2 ⇒ x3 | x3 ⇒ x4 | x4 ⇒ x5 | x5 ⇒ x6 | x6 ⇒ x7 | x7 ⇒ x8 + | x8 ⇒ x9 | x9 ⇒ xA | xA ⇒ xB | xB ⇒ xC | xC ⇒ xD | xD ⇒ xE | xE ⇒ xF | xF ⇒ x0 ]. + + +record byte8 : Type ≝ + { + b8h: exadecim; + b8l: exadecim + }. + +notation "〈x,y〉" non associative with precedence 80 + for @{ 'mk_byte8 $x $y }. +interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y). + +definition andb ≝ λa,b.match a with [ true ⇒ b | _ ⇒ false ]. + +definition eq_b8 ≝ λb1,b2:byte8.andb (eq_ex (b8h b1) (b8h b2)) (eq_ex (b8l b1) (b8l b2)). +definition succ_b8 ≝ +λb:byte8.match eq_ex (b8l b) xF with + [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b)) + | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ]. + +record word16 : Type ≝ + { + w16h: byte8; + w16l: byte8 + }. + +(* \langle \rangle *) +notation "〈x:y〉" non associative with precedence 80 + for @{ 'mk_word16 $x $y }. +interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y). + + + +definition succ_w16 ≝ +λw:word16. + match eq_b8 (w16l w) (mk_byte8 xF xF) with + [ true ⇒ mk_word16 (succ_b8 (w16h w)) (succ_b8 (w16l w)) + | false ⇒ mk_word16 (w16h w) (succ_b8 (w16l w)) ]. + +inductive eq (A:Type) (a:A) : A → Prop ≝ refl_eq : eq A a a. + +interpretation "aa" 'eq t a b = (eq t a b). + + -- 2.39.2