The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Pierre Casteran 
<pierre.casteran AT labri.fr>:

 I found some solution, but it looks quite awkward.
Is there a better solution?

 a) generalize all theorems one wants to use
 b) generalize all subterms leading to long computations.
 c) clear some dangerous hypotheses
 d) then proceed as usual.

In the tower example, this gives :


Lemma tower_S : forall n, tower (S n) = exp2 (tower n).
 simpl;auto.
Qed.

Goal 23 < exp2 (tower 5) -> 24 <= (tower 6).
Proof.
  intro H.
  generalize (tower_S 5).
  generalize H.
  generalize (tower 5) (tower 6).
  clear H;induction 2;auto.
Qed.


Pierre



> Hello,
>
>  Is it possible to rewrite or replace a term with another, whithout
>  reducing them?
>
>  In the following little example, I could not manage to rewrite
> the lemma tower_S whithout going into very large computations.
>
>
> Pierre
>
>
> Fixpoint exp2 (n:nat) : nat :=
>  match n with 0 => 1
>             | S p => 2 * (exp2 p)
>  end.
>
> Fixpoint tower (n:nat) : nat :=
>   match n with 0 => 1
>              | S p => exp2 (tower p)
>   end.
>
>
> Lemma tower_S : forall n, tower (S n) = exp2 (tower n).
>  simpl;auto.
> Qed.
>
>
> Goal 23 < exp2 (tower 5) -> 24 <= (tower 6).
> Proof.
>  intro H.
>  (* loops :
>  rewrite (tower_S 5).
>  *)
>  (* loops :
>  replace (tower 6) with (exp2 (tower 5)).
>  *)
>  Opaque tower exp2.
>  (* loops :
>  rewrite (tower_S 5).
>  *)
>
>
>
>
> --
> Pierre Casteran
>
> http://www.labri.fr/Perso/~casteran/
>
> (+33) 540006931
>
> ----------------------------------------------------------------
> This message was sent using IMP, the Internet Messaging Program.
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.