The Coq mailing list

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

Selon Nicolas Magaud 
<nmagaud AT cse.unsw.edu.au>:

Hello Nicolas,

 Thanks for your answer.

 If you modify slightly this example, there can remain some problems:

Lemma L :  tower 6 = exp2 (tower 5).
 rewrite tower_S.
 reflexivity.
Qed.

 Goal 23 < exp2 (tower 5) -> 24 <= (tower 6).
Proof.
 intro H.
 rewrite L.  (* "loops" (in fact, goes into a very large computation *)

This last example is closer to the original problem I simplified
in my mail of yesterday, when the equality I wanted to eliminate
hold between huge numbers (very much bigger than the number of atoms
 in the Universe :-) )

 Happily, it could be solved using "generalize".

Nevertheless, it is interesting to classify tactics depending on the
reductions they do before applying inference rules.

For instance, if N is a term reducible to a very large number,
 a goal like  N=N is solved immediately with reflexivity, whilst a
call to trivial can go into a computation no human will see the end of
which.

Cheers,

Pierre


> Hi Pierre,
>
> Just for fun, I tried out your little example.
> With "Coq 8.0cvs (checked out on 24/01/2005)",
> I used the tactic "rewrite tower_S" instead of
> "rewrite (tower_S 5) and it did rewrite "(tower 6)"
> into "exp2 (tower 5)" without struggling to compute anything first.
> In case, there's several choices for where to rewrite, pattern should
> help you out.
>
> The full script eventually boils down to "intro H. rewrite tower_S.
> assumption."
>
> Cheers,
> Nicolas
>
> | 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.