The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

I was wondering if lemma1, lemma2 and lemma3 below were doable:
Thanks in advance.

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

Lemma lemma2 (ord : nat)(s : ST)(sl : list ST)(H : order s = ord) :
                 find ord (s::sl) 0 = find ord sl 1.
Proof.
Admitted.

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

-- 
View this message in context: 
http://www.nabble.com/Problems-with-tail-recursion.-tp22477726p22477726.html
Sent from the Coq mailing list archive at Nabble.com.