Library Coq.micromega.Zify

Require Import ZifyClasses.
Require Export ZifyInst.
Require Import InitialRing.

Ltac zify_unop_core t thm a :=
 
 pose proof (thm a);
 
 let z := fresh "z" in set (z:=t a) in *; clearbody z.

Ltac zify_unop_var_or_term t thm a :=
 
 let za := fresh "z" in
 (rename a into za; rename za into a; zify_unop_core t thm a) ||
 
 (remember a as za; zify_unop_core t thm za).

Ltac zify_unop t thm a :=
 
 
 let isz := isZcst a in
 match isz with
  | true =>
    let u := eval compute in (t a) in
    change (t a) with u in *
  | _ => zify_unop_var_or_term t thm a
 end.

Ltac zify_unop_nored t thm a :=
 
 let isz := isZcst a in
 match isz with
  | true => zify_unop_core t thm a
  | _ => zify_unop_var_or_term t thm a
 end.

Ltac zify_binop t thm a b:=
 
 let isza := isZcst a in
 match isza with
   | true => zify_unop (t a) (thm a) b
   | _ =>
       let za := fresh "z" in
       (rename a into za; rename za into a; zify_unop_nored (t a) (thm a) b) ||
       (remember a as za; match goal with
         | H : za = b |- _ => zify_unop_nored (t za) (thm za) za
         | _ => zify_unop_nored (t za) (thm za) b
        end)
 end.


Ltac applySpec S :=
  let t := type of S in
  match t with
  | @BinOpSpec _ _ ?Op _ =>
    let Spec := (eval unfold S, BSpec in (@BSpec _ _ Op _ S)) in
    repeat
      match goal with
      | H : context[Op ?X ?Y] |- _ => zify_binop Op Spec X Y
      | |- context[Op ?X ?Y] => zify_binop Op Spec X Y
      end
  | @UnOpSpec _ _ ?Op _ =>
    let Spec := (eval unfold S, USpec in (@USpec _ _ Op _ S)) in
    repeat
      match goal with
      | H : context[Op ?X] |- _ => zify_unop Op Spec X
      | |- context[Op ?X ] => zify_unop Op Spec X
      end
  end.

Ltac zify_post_hook := idtac.

Ltac zify := zify_op ; (iter_specs applySpec) ; zify_post_hook.