The Coq mailing list

["JAEGER, Eric (SGDN)" <eric.jaeger AT sgdn.gouv.fr>]

Hi,

 

I have quickly investigated possible transformations (reduction, unfolding, rewriting) under a binder. When the binder do not bind a free variable in the term (e.g. f(0) in forall (n:nat), ...f(0)...) it is possible to unfold, reduce and rewrite this term. When the binder capture a free variable (e.g. f(n) in forall (n:nat), ...f(n)...) it is possible to unfold but not to reduce (except if after unfolding the bound variable disappear, e.g. by defining f(n m:nat)=f' n) or to rewrite - the situation appears similar either using a forall or a match (forall (n:nat) bind n, while match n as 0 =>... | S n' => ... bind n').

 

So here is my question: Provided I have a function leb:bool->bool s.t. leb_0:forall (n:nat), leb 0 n=true holds, is there a tactic in Coq to rewrite a term of the form (leb 0 n) under a binder capturing n, without having to first eliminate this binder? In other words, is there a way to prove the theorem test below WITHOUT using intros / destruct?

 

Variable leb:nat->nat->bool.

Axiom leb_0:forall (n:nat), leb 0 n=true.

Theorem test:forall (n:nat), match n with
                        | 0 => leb 0 0=leb 0 (S n)
                        | S n' => leb 0 n'=leb 0 n
                       end.
Proof.
 intros n.
 destruct n as [| n].
   rewrite leb_0; rewrite leb_0; apply refl_equal.
   rewrite leb_0; rewrite leb_0; apply refl_equal.
Qed.

 

    Thanks for your answers, Eric