Module Coq.Rewrite

module Rewrite: sig .. end


The rewriting tactics used in aac_rewrite, build as handlers of the usual setoid_rewrite

Datatypes


type hypinfo = {
   hyp : Term.constr; (*the actual constr corresponding to the hypothese*)
   hyptype : Term.constr; (*the type of the hypothesis*)
   context : Term.rel_context; (*the quantifications of the hypothese*)
   body : Term.constr; (*the body of the hypothese*)
   rel : Coq.Relation.t; (*the relation*)
   left : Term.constr; (*left hand side*)
   right : Term.constr; (*right hand side*)
   l2r : bool; (*rewriting from left to right*)
}
We keep some informations about the hypothesis, with an (informal) invariant:
val get_hypinfo : Term.constr ->
l2r:bool ->
?check_type:(Term.types -> bool) ->
(hypinfo -> Proof_type.tactic) -> Proof_type.tactic
get_hypinfo H l2r ?check_type k analyse the hypothesis H, and build the related hypinfo, in CPS style. Moreover, an optionnal function can be provided to check the type of every free variable of the body of the hypothesis.

Rewriting with bindings

The problem : Given a term to rewrite of type H :forall xn ... x1, t, we have to instanciate the subset of xi of type carrier. subst : (int * constr) is the mapping the De Bruijn indices in t to the constrs. We need to handle the rest of the indexes. Two ways :

Both these terms have the same type.
val build : hypinfo ->
(int * Term.constr) list ->
(Term.constr -> Proof_type.tactic) -> Proof_type.tactic
build the constr to rewrite, in CPS style, with lambda abstractions
val build_with_evar : hypinfo ->
(int * Term.constr) list ->
(Term.constr -> Proof_type.tactic) -> Proof_type.tactic
build the constr to rewrite, in CPS style, with evars
val rewrite : ?abort:bool ->
hypinfo ->
(int * Term.constr) list ->
(Proof_type.tactic -> Proof_type.tactic) -> Proof_type.tactic
rewrite ?abort hypinfo subst builds the rewriting tactic associated with the given subst and hypinfo, and feeds it to the given continuation. If abort is set to true, we build tclIDTAC instead.