The Coq mailing list

[julien forest <(e29315a54f%hidden_head%e29315a54f)forest(e29315a54f%hidden_at%e29315a54f)ensiie.fr(e29315a54f%hidden_end%e29315a54f)>]

Hi,


On Sun, 13 May 2012 23:06:11 +0200
Nuno Gaspar 
<(e29315a54f%hidden_head%e29315a54f)nmpgaspar(e29315a54f%hidden_at%e29315a54f)gmail.com(e29315a54f%hidden_end%e29315a54f)>
 wrote:

> Hello.
> 
> Consider the following trivial definitions:
> 
> Inductive X : Type := Const: nat -> X.
> Definition projX (x:X) : nat :=
>   match x with
>     | Const n => n
>   end.
> 
> 
> Function f (l:list X)  (id:nat) (acc:list X) {struct l} : option (X *
> list X) :=
>   match l with
>     | nil    => None
>     | c :: r => if beq_nat (projX c) id then Some ((c, r :: acc))
> else f r id (c :: acc)
>   end.
This Function does not typecheck. I suppose you meaned (Some ((c, r ++
acc)) for the rest of the script.

> 
> The above function simply looks for an element whose projection is
> equal to the given id. The problem arises due to the use of an
> accumulator - it will yield a weird induction hypothesis..
> 
> For instance, in this following lemma
> 
> Lemma fact:
>   forall l id X c r,
>   f l id X = Some (c,r) ->
>   X = nil ->    (*there's a reason for not directly including 'nil'
> in the function call above, but can be ignored for this question...*)
>   forall x, In x l <-> In x (c :: r).
> Proof.
>   intros.
>   functional induction f l id X0; inversion H; subst; clear H.
>   Case "branch true".
>     admit. (*trivially true*)
>   Case "branch false".
>     (*weird induction hyp*)
> Qed.
Your statement is too strict. You can state and prove the following
lemma : 


Lemma gen_fact:
  forall l id X c r,
  f l id X = Some (c,r) ->
  forall x, (In x l \/  In x X)  <-> In x (c :: r). 
Proof.
  intros l id X0.
  functional induction f l id X0; intros; inversion H; subst; clear H. 
  admit. (*trivially true*)
  assert (IH':=IHo _ _  H1);clear IHo.
  split;intros H.
  destruct H. 
  simpl in H;destruct H.
  subst.
  apply IH'.
  admit.
  apply IH'.
  admit.
  apply IH'.
  admit.
  simpl in H;destruct H.
  subst.
  simpl in *.
  admit.
  admit.
Qed.
Where the admitted proofs are just trivial facts about being a member
of a list.

Then you can derive your fact lemma which is just the particular case
where X=nil. 


Best regard, 
Julien.