証明

この一週間くらい手を動かしてた、Software Foundationsの「サブシーケンスという関係は推移的である。」ということの証明が出来た!

めっさうれしい。

Inductive subseq : list nat -> list nat -> Prop :=
 | subseq_nil : subseq [] []
 | subseq_e : forall l1 l2 n, subseq l1 l2 -> subseq (n::l1) (n::l2)
 | subseq_ne : forall l1 l2 n, subseq l1 l2 -> subseq l1 (n::l2).

Theorem nil_is_subseq : 
  forall l, subseq [] l.
Proof.
  induction l. apply subseq_nil.
  apply subseq_ne. apply IHl.
Qed.

Theorem subseq_trans : forall l1 l2 l3,
  subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3.
Proof.
  intros l1 l2 l3.
  generalize dependent l1.
  generalize dependent l2.
  induction l3 as [|x l3'].  
  - intros. inversion H.  apply subseq_nil. subst. inversion H0. destruct l2. destruct l1. apply subseq_nil. inversion H3. inversion H0.
  - intros.
    inversion H0 as [|l2' l3'' n|l2' l3'' n] .  subst.
    inversion H as [|l1' l2'' n'|l1' l2'' n']. subst. apply subseq_e. apply  IHl3' with (l2:=l2').
    apply H4. apply H3.
    subst.
    apply subseq_ne. apply IHl3' with (l2:=l2'). apply H4. apply H3.   
    subst. apply subseq_ne. apply IHl3' with (l2:=l2). apply H. apply H3.
Qed.

前に読んでよー分からんかった、inversionの動きがある程度分かった気がする。
コンストラクタの単射性ってなんやねんって感じだったけど、あるコンストラクタがある引数で作られる結果は唯一だから結果から逆算出来るということなのね。