CoRN.tactics.Rational

Require Export FieldReflection.
Require Export RingReflection.
Require Export CRing_as_Ring.

Inductive AlgebraName : Type :=
|cfield : CField → AlgebraName
|cring : CRing → AlgebraName.

Ltac GetStructureName t :=
match t with
| (csg_crr (cm_crr (cg_crr (cag_crr (cr_crr ?r))))) ⇒
  match r with
  | (cf_crr ?q) ⇒ constr:(cfield q)
  | _ ⇒ constr:(cring r)
 end
end.


Ltac rational :=
match goal with
[|-@cs_eq (cs_crr ?T) ?x ?y] ⇒
 match GetStructureName T with
 |(cfield ?F) ⇒ rationalF F x y
 |(cring ?R) ⇒ (repeat (try apply csf_fun_wd);simpl;ring)

 end
end.

Tactic Notation "rstepl" constr(c) := stepl c;[idtac|rational].
Tactic Notation "rstepr" constr(c) := stepr c;[idtac|rational].