...

diff --git a/helm/software/matita/tests/unifhint.ma b/helm/software/matita/tests/unifhint.ma
new file mode 100644 (file)
index 0000000..6d0c733
--- /dev/null
+++ b/helm/software/matita/tests/unifhint.ma
@@ -0,0 +1,92 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+record group : Type ≝ {
+  gcarr :> Type;
+  gmult : gcarr → gcarr → gcarr; 
+  gopp  : gcarr → gcarr;
+  gunit : gcarr
+}.
+
+interpretation "unif hints inverse" 'invert x = (gopp _ x).
+interpretation "unif hing times" 'times x y = (gmult _ x y).
+notation "𝟙" non associative with precedence 90 for @{ 'unit }.
+interpretation "unif hint unit" 'unit = (gunit _).
+
+include "nat/nat.ma".
+include "list/list.ma".
+
+inductive Expr : Type ≝
+  | Evar : nat → Expr
+  | Eopp : Expr → Expr
+  | Eunit : Expr
+  | Emult : Expr → Expr → Expr.
+  
+let rec sem (g : group) (e : Expr) (gamma : list (gcarr g)) on e : gcarr g ≝ 
+  match e with
+  [ Evar n ⇒ nth ? gamma 𝟙 n
+  | Eopp x ⇒ (sem g x gamma) ^ -1
+  | Eunit ⇒ 𝟙
+  | Emult x y ⇒ (sem g x gamma) * (sem g y gamma)].
+  
+notation "〚term 19 x, term 19 g〛" non associative with precedence 90 
+for @{ 'sem $x $g}.
+interpretation "unif hint sem" 'sem x g = (sem _ x g). 
+  
+axiom P : ∀g:group. gcarr g → Prop.
+axiom tac : Expr → Expr.
+axiom start : ∀g,x,G.P g 〚x,G〛 → Prop.
+
+notation "@ t" non associative with precedence 90 for @{ (λx.x) $t }.
+
+
+unification hint 0 (∀g:group.∀x:Expr.∀G:list (gcarr g). 〚Eopp x,G〛 = (@〚x,G〛) ^-1).
+unification hint 0 (∀g:group.∀x,y.∀G:list (gcarr g). 〚Emult x y,G〛 = (@〚x,G〛) * (@〚y,G〛)).
+unification hint 0 (∀g:group.∀G:list (gcarr g). 〚Eunit,G〛 = 𝟙).
+unification hint 2 (∀g:group.∀G:list (gcarr g).∀x:gcarr g. 〚(Evar 0), (x :: G)〛 = @x).
+unification hint 3 (∀g:group.∀G:list (gcarr g).∀n.∀x:gcarr g.(@〚Evar n, G〛)=
+   (〚(Evar (S n)), (x :: G)〛) ) . 
+
+lemma test : ∀g:group.∀x,y:gcarr g. ∀h:P ? ((𝟙 * x) * (x^-1 * y)). 
+   start g ? ? h.
+ 
+   y == [| ?, x::? |]  
+   
+   〚Evar n, G〛 
+   
+   
+   int: 〚(Evar (S n)), (x :: G)〛 = 〚Evar n, G〛
+                             nth (m) (G)          = 〚Evar n, G〛
+
+
+∀x,Γ. [| B 0, x::Γ |] = x
+∀n,y,Γ. [| B n, Γ |] = [| B (S n), y::Γ |] 
+∀e,f. [| Add e f, Γ |] = [| e, Γ |] + [| f, Γ |]
+
+
+x + x = [| ?1, ?2 |]
+
+x = [| ?1,?2 |]
+?1 ≝ B 0
+?2 ≝ x::?3
+
+x = [| ?4, y::x::?3 |]
+
+[| ?4, x::?3 |] =?= [| B (S ?n), ?y::?Γ |]
+x =?= [| B ?n, ?Γ |]
+
+
+x  =?=   E
+
+x  =?=  ?,   ? =?= E

diff --git a/helm/software/matita/tests/unifhint_simple.ma b/helm/software/matita/tests/unifhint_simple.ma
new file mode 100644 (file)
index 0000000..48ad5c4
--- /dev/null
+++ b/helm/software/matita/tests/unifhint_simple.ma
@@ -0,0 +1,79 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+record group : Type ≝ {
+  gcarr :> Type;
+  gmult : gcarr → gcarr → gcarr; 
+  gopp  : gcarr → gcarr;
+  gunit : gcarr
+}.
+
+interpretation "unif hints inverse" 'invert x = (gopp _ x).
+interpretation "unif hing times" 'times x y = (gmult _ x y).
+notation "𝟙" non associative with precedence 90 for @{ 'unit }.
+interpretation "unif hint unit" 'unit = (gunit _).
+
+inductive Expr (g : group) : Type ≝
+  | Evar : gcarr g → Expr g
+  | Eopp : Expr g → Expr g
+  | Eunit : Expr g
+  | Emult : Expr g → Expr g → Expr g.
+  
+let rec sem (g : group) (e : Expr g) on e : gcarr g ≝ 
+  match e with
+  [ Evar x ⇒ x
+  | Eopp x ⇒ (sem g x) ^ -1
+  | Eunit ⇒ 𝟙
+  | Emult x y ⇒ (sem g x) * (sem g y)].
+  
+notation "〚x〛" non associative with precedence 90 for @{ 'sem $x }.
+interpretation "unif hint sem" 'sem x = (sem _ x). 
+  
+axiom P : ∀g:group. gcarr g → Prop.
+axiom tac : ∀g:group. Expr g → Expr g.
+axiom start : ∀g,x.P g 〚x〛 → Prop.
+
+
+include "logic/equality.ma".
+
+notation "@ t" non associative with precedence 90 for @{ (λx.x) $t }.
+
+unification hint (∀g:group.∀x:g. 〚Evar ? x〛 = x).
+unification hint (∀g:group.∀x. 〚Eopp g x〛 = (@〚x〛) ^-1).
+unification hint (∀g:group.∀x,y. 〚Emult g x y〛 = (@〚x〛) * (@〚y〛)).
+
+lemma test : ∀g:group.∀x,y:g. ∀h:P ? (x * (x^-1 * y)). start g ? h.
+ 
+
+
+∀x,Γ. [| B 0, x::Γ |] = x
+∀n,y,Γ. [| B n, Γ |] = [| B (S n), y::Γ |] 
+∀e,f. [| Add e f, Γ |] = [| e, Γ |] + [| f, Γ |]
+
+
+x + x = [| ?1, ?2 |]
+
+x = [| ?1,?2 |]
+?1 ≝ B 0
+?2 ≝ x::?3
+
+x = [| ?4, y::x::?3 |]
+
+[| ?4, x::?3 |] =?= [| B (S ?n), ?y::?Γ |]
+x =?= [| B ?n, ?Γ |]
+
+
+x  =?=   E
+
+x  =?=  ?,   ? =?= E
\ No newline at end of file