The Coq mailing list

[Marthe Bonamy <marthe.bonamy AT ens-lyon.fr>]

Hi Michael,

I think the best way to do that is to use Ltac (I don't know if you are familiar with it?).

For example, with 

Ltac changep :=
match goal with
  |- 1 <= asr ?a ?b => 
    let c:= eval compute in a  in
    match (eval compute in (b-1)) with
      0 => 
         change (1 <= asr c (1+(b-1)));
         rewrite asr_1 ; intuition
   | ?d => 
         change (1 <= asr c (1+d)) ;
         rewrite asr_2 with (x:=c) (y:=1) (z:=d) ; intuition ;
         rewrite asr_1 with (x:=c) ; intuition
    end
end.

(which basically automatises what you did manually, and checks the case when b=1, in order to make sure it will stop)

all you have to do is invoke it "repeat changep"

and then you only have to prove 1 <= 625/2, which you can do manually or through another tactic.

Ltac is really useful for such things.

Hope this helps :-)

Cheers,

Marthe

On 5 July 2010 17:53, Michael <michaelschausten AT googlemail.com> wrote:

Thank you, the references you gave me helped me to complete the proof. However,
it still looks quite complicated:

Lemma test1 :
 1 <= asr 10000 5.
Proof.
change (1 <= asr 10000 (1 + 4)).
rewrite asr_2 with (x:=10000) (y:=1) (z:=4).
rewrite asr_1 with (x:=10000).
change (1 <= asr 5000 (1 + 3)).
rewrite asr_2 with (x:=5000) (y:=1) (z:=3).
rewrite asr_1 with (x:=5000).
change (1 <= asr 2500 (1 + 2)).
rewrite asr_2 with (x:=2500) (y:=1) (z:=2).
rewrite asr_1 with (x:=2500).
change (1 <= asr 1250 (1 + 1)).
rewrite asr_2 with (x:=1250) (y:=1) (z:=1).
rewrite asr_1 with (x:=1250).
change (1 <= asr 625 1).
rewrite asr_1.
change (1 <= 312).
intuition.
intuition.
intuition.
intuition.
intuition.
intuition.
intuition.
intuition.
intuition.
intuition.
Save.

For each step of simplification, I have to manually calculate the values for
[change] and [rewrite], which works of course, but is a lot of work.
- Is there a way to let Coq automatically determine which values for x,y,z
will match?
- Can I solve all 10 subgoals I have in the end with a single call of intuition
at once? I found out how to use [repeat], but it only seems to apply a tactic
multiple times to a single subgoal, not to multiple subgoals at once.