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;
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 ≝
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 > "ident a ≟ term 90 b term 20 c"
52 non associative with precedence 90 for
53 @{ let ${ident a} ≝ $b in $c }.
55 unification hint 0 (∀g:group.∀x:Expr.∀G:list (gcarr g).
57 (* ------------------------------------ *)
61 unification hint 0 (∀g:group.∀x,y.∀G:list (gcarr g).
64 (* ------------------------------------ *)
65 〚Emult x y,G〛 = V1 * V2).
67 unification hint 0 (∀g:group.∀G:list (gcarr g).
69 (* ------------------------------------ *)
72 unification hint 2 (∀g:group.∀G:list (gcarr g).∀x:gcarr g.
75 (* ------------------------------------ *)
76 〚(Evar 0), (x :: G)〛 = V).
78 unification hint 3 (∀g:group.∀G:list (gcarr g).∀n.∀x:gcarr g.
81 (* ------------------------------------ *)
82 〚(Evar (S n)), (x :: G)〛 = V) .
84 (* Esempio banale di divergenza
85 unification hint 0 (∀g:group.∀G:list (gcarr g).∀x.
87 ------------------------------------
91 include "nat/plus.ma".
92 unification hint 0 (∀x,y.S x + y = S (x + y)).
95 axiom F : ∀n,k.T (S (n + k)) → Prop.
96 lemma diverge: ∀k,k1.∀h:T (? + k).F ? k1 h.
100 lemma test : ∀g:group.∀x,y:gcarr g. ∀h:P ? ((𝟙 * x) * (x^-1 * y)).
103 lemma test : ∀g:group.∀x,y:gcarr g. ∀h:P ? ((𝟙 * x) * (x^-1 * y)).
111 int: 〚(Evar (S n)), (x :: G)〛 = 〚Evar n, G〛
112 nth (m) (G) = 〚Evar n, G〛
115 ∀x,Γ. [| B 0, x::Γ |] = x
116 ∀n,y,Γ. [| B n, Γ |] = [| B (S n), y::Γ |]
117 ∀e,f. [| Add e f, Γ |] = [| e, Γ |] + [| f, Γ |]
126 x = [| ?4, y::x::?3 |]
128 [| ?4, x::?3 |] =?= [| B (S ?n), ?y::?Γ |]