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 : EConstr.constr;`	`(*`	the actual constr corresponding to the hypothese	`*)`
`hyptype : EConstr.constr;`	`(*`	the type of the hypothesis	`*)`
`context : EConstr.rel_context;`	`(*`	the quantifications of the hypothese	`*)`
`body : EConstr.constr;`	`(*`	the body of the hypothese	`*)`
`rel : Coq.Relation.t;`	`(*`	the relation	`*)`
`left : EConstr.constr;`	`(*`	left hand side	`*)`
`right : EConstr.constr;`	`(*`	right hand side	`*)`
`l2r : bool;`	`(*`	rewriting from left to right	`*)`

}

We keep some informations about the hypothesis, with an (informal) invariant:

typeof hyp = typ
typ = forall context, body
body = rel left right

val get_hypinfo : Environ.env ->
       Evd.evar_map ->
       ?check_type:(EConstr.types -> bool) ->
       EConstr.constr -> l2r:bool -> hypinfo

get_hypinfo ?check_type H l2r analyse the hypothesis H, and build the related hypinfo. 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 :

either using fresh evars and rewriting H tn ?1 tn-2 ?2
either building a term like fun 1 2 => H tn 1 tn-2 2

Both these terms have the same type.

val build : hypinfo -> (int * EConstr.constr) list -> EConstr.constr

build the constr to rewrite, with lambda abstractions

build the constr to rewrite, in CPS style, with evars

val rewrite : ?abort:bool ->
       hypinfo -> (int * EConstr.constr) list -> unit Proofview.tactic

rewrite ?abort hypinfo subst builds the rewriting tactic associated with the given subst and hypinfo. If abort is set to true, we build tclIDTAC instead.