Nachweisende Erhöhung Iota in Coq

Question

Ich bin auf ein Ziel stecken.

Angenommen, wir die folgende Definition haben:

Fixpoint iota (n : nat) : list nat := 
    match n with 
    | 0 => [] 
    | S k => iota k ++ [k] 
    end. 

Und wollen wir beweisen:

Theorem t1 : forall n, In n (iota n) -> False. 
Proof. 
    intros. 
    induction n. 
    - cbn in H. contradiction. 
    - cbn in H. apply app_split in H. 
     Focus 2. unfold not. intros. 
     unfold In in H0. destruct H0. assert (~(n = S n)) by now apply s_inj. 
     contradiction. 
     apply H0. 
     apply IHn. 

:

Theorem t1 : forall n, In n (iota n) -> False.

Bisher habe ich die folgenden Managed Ich habe diese beiden Lemmas benutzt, Beweise weggelassen:

Axiom app_split : forall A x (l l2 : list A), In x (l ++ l2) -> not (In x l2) -> In x l. 
Axiom s_inj  : forall n, ~(n = S n). 

Allerdings bin ich ganz fest, ich brauche die irgendwie zeigen: In n (iota n) vorausgesetzt In (S n) (iota n).

Answer 1

Wie Sie die Tatsache beobachtet haben, dass die n in In n und der in iota n in Lockstep in Ihrer Erklärung sind, macht die harte Induktionsvoraussetzung aufzurufen (wenn nicht sogar völlig nutzlos).

Der Trick hier ist, eine allgemeinere Aussage zu beweisen, als die, die Sie tatsächlich interessiert, die diese Abhängigkeit zwischen den zwei n s bricht. Ich würde vorschlagen:

Theorem t : forall n k, n <= k -> In k (iota n) -> False. 

, von dem Sie t1 als logische Folge ableiten können:

Corollary t1 : forall n, In n (iota n) -> False. 
intro n; apply (t n n); reflexivity. 
Qed. 

Wenn man sich den Beweis t spähen möchten, können Sie have a look at this self-contained gist