list - Function- and Type substitutions or Views in Coq -

i proved theorems lists, , extracted algorithms them. want use heaps instead, because lookup , concatenation faster. achieve use custom definitions extracted list type. in more formal way, ideally without having redo of proofs. lets have type

heap : set -> set 

and isomorphism

f : forall a, heap -> list a. 

furthermore, have functions h_app , h_nth, such that

h_app (f a) (f b) = f (a ++ b) 

and

h_nth (f a) = nth 

on 1 hand, have replace every list-recursion specialized function mimics list recursion. on other hand, beforehand want replace ++ , nth h_app , h_nth, extracted algorithms faster. problem use tactics simpl , compute in places, fail if replace in proof code. have possibility "overload" functions afterwards.

is possible?

edit: clarify, similar problem arises numbers: have old proofs use nat, numbers getting large. using binnat better, possible use binnat instead of nat in old proofs without modification? (and especially, replace inefficient usages of + more efficient definition binnat?)

just sake of clarity, take heap must this:

inductive heap : type := | node : heap -> -> heap -> heap | leaf : heap a. 

with f being defined as

fixpoint f (h : heap a) : list :=   match h   | node h1 h2 => f h1 ++ :: f h2   | leaf => []   end. 

if case, f not define isomorphism between heap a , list a a. instead, can find function g : forall a, list -> heap a such that

forall (l : list a), f (g l) = l 

nevertheless, both heap , list equivalent in sense when used implement same abstraction, namely sets of elements of type.

there precise , formal way in can validate idea in languages have parametric polymorphism, such coq. principle, known parametricity, says parametrically polymorphic functions respect relations impose on types instantiate them with.

this little bit abstract, let's try make more concrete. suppose have function on lists (say, foo) uses ++ , nth. able replace foo equivalent version on heap using parametricity, need make foo's definition polymorphic, abstracting on functions on lists:

definition foo (t : set -> set)                (app : forall a, t -> t -> t a)                (nth : forall a, t -> nat -> option a)                (l : t a) : t :=   (* ... *) 

you first prove properties of foo instantiating on lists:

definition list_foo := foo list @app @nth.  lemma list_foo_lemma : (* statement *). 

now, because h_app , h_nth compatible list counterparts, , because foo polymorphic, theory of parametricity says can prove

definition h_foo := foo heap @h_app @h_nth.  lemma foo_param : forall (h : heap a),                     f (h_foo h) = list_foo (f h). 

with lemma in hand, should possible transport properties of list_foo similar properties of h_foo. instance, trivial example, can show h_app associative, conversion list:

forall (h1 h2 h3 : heap a),   list_foo (h_app h1 (h_app h2 h3)) =   list_foo (h_app (h_app h1 h2) h3). 

what's nice parametricity applies any parametrically polymorphic function: long appropriate compatibility conditions hold of types, should possible relate 2 instantiations of given function in similar fashion foo_param.

there 2 problems, however. first 1 having change base definitions polymorphic ones, not bad. what's worse, though, though parametricity ensures possible prove lemmas such foo_param under conditions, coq not give free, , still need show these lemmas hand. there 2 things alleviate pain:

1. there's parametricity plugin coq (coqparam) should deriving boilerplate proofs automatically. have never used it, though, can't how easy use.

2. the coq effective algebra library (or coqeal, short) uses parametricity prove things efficient algorithms while reasoning on more convenient ones. in particular, define refinements allow 1 switch between nat , binnat, suggested. internally, use infrastructure based on type-class inference, adapt original example, heard migrating implementation use coqparam instead.