The Coq mailing list

[Cedric Auger <Cedric.Auger AT lri.fr>]

Edsko de Vries a e'crit :
> What's difficult about them? I tried lemma1 and lemma2, and they go 
> through easily enough. Where do you get stuck?
>
> (BTW, compare_nat is eq_nat_dec from the Arith library).
>
> Edsko
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/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
A more constructive answer ;)

Require Import List.
Require Import TheoryList.
Require Import Max.

Definition max_list (l : list nat) : nat := fold_left max l 0.

Inductive ST : Type :=
| arr : list ST -> ST.

Function order (s : ST) : nat :=
match s with
| arr sl => match sl with
| nil => 0
| _ => 1 + max_list (map order sl)
end
end.

Lemma compare_nat : forall (n m : nat), {n = m} + {n <> m}.
Proof.
Admitted.

Fixpoint find (ord : nat) (sl : list ST) (l : nat) {struct sl} : nat :=
match sl with
| nil => l
| s :: sl0 =>
if compare_nat (order s) ord then find ord sl0 (l + 1) else l
end.

Lemma lemma1 (ord : nat)(sl : list ST)(l : nat) :
find ord sl (S l) = S (find ord sl l).
Proof.
intros; revert l.
induction sl; simpl.
auto.
intro l; destruct (compare_nat (order a) ord); auto.
Qed.

Lemma lemma2 (ord : nat)(s : ST)(sl : list ST)(H : order s = ord) :
find ord (s::sl) 0 = find ord sl 1.
Proof.
intros; simpl; rewrite H; destruct (compare_nat ord ord).
auto.
destruct n; auto.
Qed.

Lemma lemma3 (ord : nat)(s : ST)(sl : list ST)(H : order s = ord)(l : nat) :
find ord (s::sl) l = S (find ord sl l).
Proof.
intros; simpl; rewrite H; destruct (compare_nat ord ord).
rewrite <- lemma1; rewrite (plus_n_O l); rewrite (plus_n_Sm l O);
rewrite <- (plus_n_O l); auto.
destruct n; auto.
Qed.

The last lemma can be cleaned, and I didn't use omega...

--
Ce'dric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay