Module AAC_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 : AAC_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:

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

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 :

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 * 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.