Module abgroup

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.


Index
This page has been generated by coqdoc