proposition: Lemma inter_diss : forall x l lh lt s, afs_filt (lh ++ s :: lt) l = intersperse s (map (afs_filt (lh ++ x :: lt)) (dissect (length lh) l)).
proof: Proof. clear; intros; set (ds := dissect (length lh) l); assert (Heq: dissect (length lh) l = ds); [ reflexivity | clearbody ds ]. revert l Heq; induction ds; intros; [ apply dissect_not_nil in Heq; contradiction Heq |]. revert a l Heq; induction a; intros. destruct l; simpl in Heq; [ injection Heq; intros; subst; reflexivity |]; case_eq (Nat.eqb (length lh) n); intros Hn; rewrite Hn in Heq; [| destruct (dissect (length lh) l); discriminate Heq ]; injection Heq; clear Heq; intros Heq; destruct ds; [ apply dissect_not_nil in Heq; contradiction Heq |]; apply Nat.eqb_eq in Hn; rewrite <- Hn; clear Hn; simpl; rewrite nth_in; f_equal; apply IHds; assumption. destruct l; simpl in Heq; [ discriminate Heq |]; case_eq (Nat.eqb (length lh) n); intros Hn; rewrite Hn in Heq; [ discriminate Heq | apply Nat.eqb_neq in Hn ]; case_eq (dissect (length lh) l); [ intros G; apply dissect_not_nil in G; contradiction G |]; intros; rewrite H in Heq; injection Heq; intros; subst; apply IHa in H; clear IHds IHa Heq. assert (nth_error (lh ++ s :: lt) a = nth_error (lh ++ x :: lt) a); [ revert a Hn; clear; induction lh; simpl; intros; [ destruct a; [ contradiction Hn |]; reflexivity | destruct a0; [ reflexivity |]; apply IHlh; intros H; contradiction Hn; rewrite H; reflexivity ]|]; simpl; rewrite H0; destruct ds; [| destruct a0 ]; rewrite H; destruct (nth_error (lh ++ x :: lt) a); reflexivity. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)