...

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 (file)
index 0000000..3aafc35
--- /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 (file)
index 0000000..4bd5f18
--- /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 (file)
index 0000000..7e74845
--- /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 (executable)
index 0000000..b47a750
--- /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 (file)
index 0000000..4998dd0
--- /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 (executable)
index 0000000..b0596ae
--- /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 (file)
index 0000000..b0578bf
--- /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).
+
+