]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/unifhint.ma
init_copy init_match
[helm.git] / matita / matita / tests / unifhint.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 record group : Type β‰ {
16   gcarr :> Type;
17   gmult : gcarr β†’ gcarr β†’ gcarr; 
18   gopp  : gcarr β†’ gcarr;
19   gunit : gcarr
20 }.
21
22 interpretation "unif hints inverse" 'invert x = (gopp _ x).
23 interpretation "unif hing times" 'times x y = (gmult _ x y).
24 notation "πŸ™" non associative with precedence 90 for @{ 'unit }.
25 interpretation "unif hint unit" 'unit = (gunit _).
26
27 include "nat/nat.ma".
28 include "list/list.ma".
29
30 inductive Expr : Type β‰
31   | Evar : nat β†’ Expr
32   | Eopp : Expr β†’ Expr
33   | Eunit : Expr
34   | Emult : Expr β†’ Expr β†’ Expr.
35   
36 let rec sem (g : group) (e : Expr) (gamma : list (gcarr g)) on e : gcarr g β‰ 
37   match e with
38   [ Evar n β‡’ nth ? gamma πŸ™ n
39   | Eopp x β‡’ (sem g x gamma) ^ -1
40   | Eunit β‡’ πŸ™
41   | Emult x y β‡’ (sem g x gamma) * (sem g y gamma)].
42   
43 notation "γ€šterm 19 x, term 19 gγ€›" non associative with precedence 90 
44 for @{ 'sem $x $g}.
45 interpretation "unif hint sem" 'sem x g = (sem _ x g). 
46   
47 axiom P : βˆ€g:group. gcarr g β†’ Prop.
48 axiom tac : Expr β†’ Expr.
49 axiom start : βˆ€g,x,G.P g γ€šx,Gγ€› β†’ Prop.
50
51 notation > "ident a β‰Ÿ term 90 b term 20 c" 
52 non associative with precedence 90 for 
53 @{ let ${ident a} β‰ $b in $c }.
54
55 unification hint 0 (βˆ€g:group.βˆ€x:Expr.βˆ€G:list (gcarr g). 
56            V β‰Ÿ γ€šx,Gγ€›
57 (* ------------------------------------ *)
58        γ€šEopp x,Gγ€› = V^-1).
59
60
61 unification hint 0 (βˆ€g:group.βˆ€x,y.βˆ€G:list (gcarr g). 
62
63        V1 β‰Ÿ γ€šx,Gγ€›        V2 β‰Ÿ γ€šy,Gγ€›
64 (* ------------------------------------ *) 
65            γ€šEmult x y,Gγ€› = V1 * V2).
66         
67 unification hint 0 (βˆ€g:group.βˆ€G:list (gcarr g). 
68
69 (* ------------------------------------ *)
70               γ€šEunit,Gγ€› = πŸ™).
71
72 unification hint 2 (βˆ€g:group.βˆ€G:list (gcarr g).βˆ€x:gcarr g. 
73
74                    V β‰Ÿ x 
75 (* ------------------------------------ *)
76           γ€š(Evar 0), (x :: G)γ€› = V).
77   
78 unification hint 3 (βˆ€g:group.βˆ€G:list (gcarr g).βˆ€n.βˆ€x:gcarr g.
79
80                V β‰Ÿ γ€šEvar n, Gγ€› 
81 (* ------------------------------------ *)  
82        γ€š(Evar (S n)), (x :: G)γ€› = V) .
83        
84 (* Esempio banale di divergenza       
85 unification hint 0 (βˆ€g:group.βˆ€G:list (gcarr g).βˆ€x.
86      V β‰Ÿ γ€šx,Gγ€› 
87  ------------------------------------      
88       γ€šx,Gγ€› = V).
89 *)
90
91 include "nat/plus.ma".
92 unification hint 0 (βˆ€x,y.S x + y = S (x + y)).
93
94 axiom T : nat β†’ Prop.
95 axiom F : βˆ€n,k.T (S (n + k)) β†’ Prop. 
96 lemma diverge: βˆ€k,k1.βˆ€h:T (? + k).F ? k1 h. 
97     ?+k    = S(?+k1)
98     S?1 + k   S(?1+k1)
99     
100 lemma test : βˆ€g:group.βˆ€x,y:gcarr g. βˆ€h:P ? ((πŸ™ * x) * (x^-1 * y)). 
101    start g ? ? h.
102
103 lemma test : βˆ€g:group.βˆ€x,y:gcarr g. βˆ€h:P ? ((πŸ™ * x) * (x^-1 * y)). 
104    start g ? ? h.
105  
106    y == [| ?, x::? |]  
107    
108    γ€šEvar n, Gγ€› 
109    
110    
111    int: γ€š(Evar (S n)), (x :: G)γ€› = γ€šEvar n, Gγ€›
112                              nth (m) (G)          = γ€šEvar n, Gγ€›
113
114
115 βˆ€x,Ξ“. [| B 0, x::Ξ“ |] = x
116 βˆ€n,y,Ξ“. [| B n, Ξ“ |] = [| B (S n), y::Ξ“ |] 
117 βˆ€e,f. [| Add e f, Ξ“ |] = [| e, Ξ“ |] + [| f, Ξ“ |]
118
119
120 x + x = [| ?1, ?2 |]
121
122 x = [| ?1,?2 |]
123 ?1 β‰ B 0
124 ?2 β‰ x::?3
125
126 x = [| ?4, y::x::?3 |]
127
128 [| ?4, x::?3 |] =?= [| B (S ?n), ?y::?Ξ“ |]
129 x =?= [| B ?n, ?Ξ“ |]
130
131
132 x  =?=   E
133
134 x  =?=  ?,   ? =?= E