The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Le 20 janv. 09 à 08:22, JAEGER, Eric (SGDN) a écrit :

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

Hi,

This is possible using the latest (8.2) setoid-rewriting tactic, but
not in the case of match constructs which are a bit hard to handle
generically. If instead of the match you used the following:

<<
Require Import Setoid.

Variable leb:nat->nat->bool.
Axiom leb_0:forall (n:nat), leb 0 n=true.

Definition nat_case (P : Type) (z : P) (s : nat -> P) (n : nat) : P :=
  match n with 0 => z | S n' => s n' end.

(** We can actually fold any (non-dependent) case analysis into a  
[nat_case] *)

Ltac fold_nat_case :=
  match goal with
    [ |- context [ match ?x with 0 => ?z | S n' => @?s n' end ] ] =>  
fold (nat_case _ z s x)
  end.

(** Defining a morphism that allows to rewrite inside the "S" case if we
   maintain logical equivalence. Of course this requires a case  
analysis. *)

Instance nat_case_morp :
  Morphism (iff ==> (pointwise_relation nat iff) ==> @eq nat ==> iff)  
(nat_case Prop).
Proof.
  reduce. subst x1. destruct y1 ; firstorder.
Qed.

(** Now we just need to rewrite with the lemma using the  
[setoid_rewrite] variant
 ([rewrite] doesn't try to go under lambdas for compatibility).  
Actually, the semantics
 of [setoid_rewrite] is a bit different: it rewrites _all_ the  
subterms that unify with
 the lemma, in their local contexts. Hence it rewrites all [leb 0 _]  
subterms in one go.
 One could use [at] to control which occurences should be rewritten. *)

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. fold_nat_case.
  setoid_rewrite leb_0.
  induction n ; reflexivity.
Qed.
>>

You can rewrite under forall/exists/you-name-it binders as well using  
the same principle.

Hope this helps,
-- Matthieu