From 4b04f3d6257efe3048e93e41201c533bc5381020 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 9 Mar 2009 18:21:23 +0000 Subject: [PATCH] ... --- helm/software/matita/tests/unifhint.ma | 92 +++++++++++++++++++ helm/software/matita/tests/unifhint_simple.ma | 79 ++++++++++++++++ 2 files changed, 171 insertions(+) create mode 100644 helm/software/matita/tests/unifhint.ma create mode 100644 helm/software/matita/tests/unifhint_simple.ma diff --git a/helm/software/matita/tests/unifhint.ma b/helm/software/matita/tests/unifhint.ma new file mode 100644 index 000000000..6d0c73350 --- /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 index 000000000..48ad5c4ce --- /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 -- 2.39.2