Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Full proof for my answer to https://stackoverflow.com/questions/44059569/
(* https://stackoverflow.com/questions/44059569/coq-goal-variable-not-transformed-by-induction-when-appearing-on-left-side-of-a/ *)
Require Import Coq.Lists.List.
Import ListNotations.
Inductive Disjoint {X : Type}: list X -> list X -> Prop :=
| disjoint_nil: Disjoint [] []
| disjoint_left: forall x l1 l2, Disjoint l1 l2 -> ~(In x l2) -> Disjoint (x :: l1) l2
| disjoint_right: forall x l1 l2, Disjoint l1 l2 -> ~(In x l1) -> Disjoint l1 (x :: l2).
Hint Constructors Disjoint.
Lemma disjoint_cons_l {X} (h : X) l1 l2 :
Disjoint (h :: l1) l2 -> Disjoint l1 l2.
Proof.
intros H; remember (h :: l1) as hl1 eqn:E.
induction H; inversion E; subst; intuition.
Qed.
Lemma disjoint_singleton {X} h (l : list X) :
Disjoint [h] l -> ~ In h l.
Proof.
intro F; remember [h] as s eqn: E.
induction F; inversion E; subst; firstorder.
Qed.
Theorem nodup_app__disjoint {X} (l: list X) :
(forall l1 l2, l = l1 ++ l2 -> Disjoint l1 l2) -> NoDup l.
Proof.
induction l as [| h l]; intros F.
- constructor.
- constructor.
+ specialize (F [h] l eq_refl).
now apply disjoint_singleton.
+ apply IHl; clear IHl; intros l1 l2 Happ.
subst; specialize (F (h :: l1) l2 eq_refl).
now apply disjoint_cons_l in F.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment