1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 record group : Type β {
17 gmult : gcarr β gcarr β gcarr;
18 gopp : gcarr β gcarr;
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 _).
28 include "list/list.ma".
30 inductive Expr : Type β
32 | Eopp : Expr β Expr
34 | Emult : Expr β Expr β Expr.
36 let rec sem (g : group) (e : Expr) (gamma : list (gcarr g)) on e : gcarr g β
38 [ Evar n β nth ? gamma π n
39 | Eopp x β (sem g x gamma) ^ -1
41 | Emult x y β (sem g x gamma) * (sem g y gamma)].
43 notation "γterm 19 x, term 19 gγ" non associative with precedence 90
45 interpretation "unif hint sem" 'sem x g = (sem _ x g).
47 axiom P : βg:group. gcarr g β Prop.
48 axiom tac : Expr β Expr.
49 axiom start : βg,x,G.P g γx,Gγ β Prop.
51 notation "@ t" non associative with precedence 90 for @{ (Ξ»x.x) $t }.
54 unification hint 0 (βg:group.βx:Expr.βG:list (gcarr g). γEopp x,Gγ = (@γx,Gγ) ^-1).
55 unification hint 0 (βg:group.βx,y.βG:list (gcarr g). γEmult x y,Gγ = (@γx,Gγ) * (@γy,Gγ)).
56 unification hint 0 (βg:group.βG:list (gcarr g). γEunit,Gγ = π).
57 unification hint 2 (βg:group.βG:list (gcarr g).βx:gcarr g. γ(Evar 0), (x :: G)γ = @x).
58 unification hint 3 (βg:group.βG:list (gcarr g).βn.βx:gcarr g.(@γEvar n, Gγ)=
59 (γ(Evar (S n)), (x :: G)γ) ) .
61 lemma test : βg:group.βx,y:gcarr g. βh:P ? ((π * x) * (x^-1 * y)).
69 int: γ(Evar (S n)), (x :: G)γ = γEvar n, Gγ
70 nth (m) (G) = γEvar n, Gγ
73 βx,Ξ. [| B 0, x::Ξ |] = x
74 βn,y,Ξ. [| B n, Ξ |] = [| B (S n), y::Ξ |]
75 βe,f. [| Add e f, Ξ |] = [| e, Ξ |] + [| f, Ξ |]
84 x = [| ?4, y::x::?3 |]
86 [| ?4, x::?3 |] =?= [| B (S ?n), ?y::?Ξ |]