Require Export group.
Require Export group_ref.
Implicit Arguments On.
Group Tactic. |
Recursive Tactic Definition MemAssoc VAR LVAR :=
Match LVAR With
| [(nilT ?)] -> false
| [(consT ? ?1 ?2)] ->
(Match ?1==VAR With
| [?1== ?1] -> true
| _ -> (MemAssoc VAR ?2)).
Recursive Tactic Definition Assoc ELT LST :=
Match LST With
| [(nilT ?)] -> Fail
| [(consT (Sprod ? nat) (Spair ? nat ?1 ?2) ?3)] ->
Match ELT==?1 With
| [?1==?1] -> ?2
| _ -> (Assoc ELT ?3).
Recursive Tactic Definition NumberAux LVAR CPT :=
Match LVAR With
| [(nilT ?1)] -> '(nilT (Sprod ?1 nat))
| [(consT ?1 ?2 ?3)] ->
Let l2 = (NumberAux ?3 '(Coq.Init.Datatypes.S CPT)) In
'(consT (Sprod ?1 nat) (Spair ?1 nat ?2 CPT) l2).
Tactic Definition Number LVAR := (NumberAux LVAR 'Coq.Init.Datatypes.O).
Recursive Tactic Definition SeekVarAux OP ID IV LVAR TRM :=
Match TRM With
| [(OP ?1 ?2)] ->
Let LVAR1 = (SeekVarAux OP ID IV LVAR ?1) In
(SeekVarAux OP ID IV LVAR1 ?2)
| [ID] -> LVAR
| [(IV ?1)] -> (SeekVarAux OP ID IV LVAR ?1)
| [?1] ->
Let res = (MemAssoc ?1 LVAR) In
Match res With
| [true] -> LVAR
| [false] -> '(!consT ? ?1 LVAR).
Tactic Definition SeekVar OP ID IV TRM :=
(SeekVarAux OP ID IV '(nilT (type_of TRM)) TRM).
Tactic Definition BuildVarList OP ID IV TRM :=
Let LVAR = (SeekVar OP ID IV TRM) In (Number LVAR).
Recursive Tactic Definition Interp OP ID IV AVAR TRM :=
Match TRM With
| [ID] -> Eid
| [(OP ?1 ?2)] ->
Let E1 = (Interp OP ID IV AVAR ?1)
And E2 = (Interp OP ID IV AVAR ?2) In '(Eop E1 E2)
| [(IV ?1)] ->
Let E = (Interp OP ID IV AVAR ?1) In '(Eiv E)
| [?1] ->
Let VARNUM = (Assoc ?1 AVAR) In '(Eatom VARNUM).
Tactic Definition AbGroupAux OP ID IV AT AVAR TRM :=
Let EXPR = (Interp OP ID IV AVAR TRM) In
Let SEXPR = '(expr_simpl OP ID IV AVAR EXPR) In
Let EQ = '(expr_simpl_ok AT AVAR EXPR) In
Cut SEXPR==TRM; [Destruct 1; Unfold expr_simpl; Simpl | Exact EQ].
Tactic Definition AbGroup1 OP ID IV AT TRM :=
Let AVAR = (BuildVarList OP ID IV TRM) In
AbGroupAux OP ID IV AT AVAR TRM.
Tactic Definition AbGroup2 OP ID IV AT TRM1 TRM2 :=
Let AVAR = (BuildVarList OP ID IV '(OP TRM1 TRM2)) In
AbGroupAux OP ID IV AT AVAR TRM1;
AbGroupAux OP ID IV AT AVAR TRM2.
Tactic Definition AbGroup OP ID IV AT :=
Match Context With
| [|- ?1==?2] -> AbGroup2 OP ID IV AT ?1 ?2; Try Reflexivity.
Recursive Tactic Definition CGroupSeekVarAux lvar trm :=
Let T = '(type_of trm) In
Match trm With
| [(zero ?)] -> lvar
| [(add ?1 ?2)] ->
Let l1 = (CGroupSeekVarAux lvar ?1) In (CGroupSeekVarAux l1 ?2)
| [(opp ?1)] -> (CGroupSeekVarAux lvar ?1)
| [(?1)] ->
Let res = (MemAssoc ?1 lvar) In
Match res With
| [(true)] -> lvar
| [(false)] -> '(consT T ?1 lvar).
Tactic Definition CGroupSeekVar trm :=
(CGroupSeekVarAux '(nilT (type_of trm)) trm).
Tactic Definition CGroupBuildVarList trm :=
Let lvar = (CGroupSeekVar trm) In (Number lvar).
Recursive Tactic Definition CGroupInterp AVAR trm :=
Match trm With
| [(zero ?)] -> Eid
| [(!add ? ?1 ?2)] ->
Let E1 = (CGroupInterp AVAR ?1)
And E2 = (CGroupInterp AVAR ?2) In '(Eop E1 E2)
| [(!opp ? ?1)] ->
Let E = (CGroupInterp AVAR ?1) In '(Eiv E)
| [?1] ->
Let VARNUM = (Assoc ?1 AVAR) In '(Eatom VARNUM).
Tactic Definition CGroup1Aux GRP AVAR TRM :=
Let EXPR = (CGroupInterp AVAR TRM) In
Let SEXPR = '(expr_simpl (!add GRP) (zero GRP) (!opp GRP) AVAR EXPR) In
Let EQ = '(expr_simpl_ok (cgroup_theory GRP) AVAR EXPR) In
Cut SEXPR==TRM; [Destruct 1; Unfold expr_simpl; Simpl | Exact EQ].
Definition cgroup_of [A:CGroup; x:A] : CGroup := A.
Tactic Definition CGroup1 TRM :=
Let AVAR = (CGroupBuildVarList TRM) In
Let GRP = '(cgroup_of TRM) In
CGroup1Aux GRP AVAR TRM.
Tactic Definition CGroup2 TRM1 TRM2 :=
Let AVAR = (CGroupBuildVarList '(add TRM1 TRM2)) In
Let GRP = '(cgroup_of TRM1) In
CGroup1Aux GRP AVAR TRM1;
CGroup1Aux GRP AVAR TRM2.
Tactic Definition CGroup GRP :=
Match Context With
| [|- ?1==?2] -> CGroup2 ?1 ?2; Try Reflexivity.