PRFA.tp4c

MPRI 2-7-2 / 2024 / Exercise session 4 / Solutions

From Coq Require Import Lia List ZArith.
Import ListNotations.

Actually products that are defined using an inductive type, can also be defined as records. For this we use parameters to records. They work like inductive parameters.
In fact, records are syntactic sugar over inductive types with one constructor that takes all the fields as arguments, and we can even give a name to that constructor.

Record prod' (A B : Type) := mkpair {
  fst' : A ;
  snd' : B
}.

Definition some_pair := mkpair _ _ 12 bool.
Print some_pair.

Actually it's annoying to have the underscores in mkpair _ 12 bool we're going to change that with the Arguments command.

Arguments mkpair {A B}.

Definition some_other_pair := mkpair false true.

You can also use do pattern matching using this constructor.

Definition to_prod {A B} (p : prod' A B) : A × B :=
  match p with
  | mkpair a b ⇒ (a, b)
  end.

Since there is only one constructor, we can also use let

Definition to_prod_alt {A B} (p : prod' A B) : A × B :=
  let 'mkpair a b := p in (a, b).

We can also use a more generic notation that doesn't require remembering the name of mkpair. It's maybe not as explicit so it's up to you to decide which version you prefer.

Definition to_prod_alt2 {A B} (p : prod' A B) : A × B :=
  let (a, b) := p in (a, b).

Generally, one uses the projections directly. They take the parameters as arguments so for convenience we declare them as implicit.

Arguments fst' {A B}.
Arguments snd' {A B}.

Definition to_prod_alt3 {A B} (p : prod' A B) : A × B :=
  (fst' p, snd' p).

EXERCISE
Show that to_prod and to_prod_alt3 produce the same result.

Lemma to_prod_eq :
  ∀ A B (p : prod' A B),
    to_prod p = to_prod_alt3 p.
Proof.
  intros A B p.
  destruct p as [a b]. reflexivity.
Qed.

We can use records to represent more complex mathematical structures by also taking types as fields. See for instance the following record representing monoids.

Class monoid := {
  m_ty :> Type ;
  m_ne : m_ty ;
  m_op : m_ty → m_ty → m_ty ;
  m_l_ne : ∀ x, m_op m_ne x = x ;
  m_r_ne : ∀ x, m_op x m_ne = x ;
  m_assoc : ∀ x y z, m_op (m_op x y) z = m_op x (m_op y z)
}.

EXERCISE
Define a record for groups.

Class group := {
  g_mon :> monoid ;
  g_inv : ∀ x, ∃ y, m_op x y = m_ne ∧ m_op y x = m_ne
}.

Notation "a ** b" := (m_op a b) (at level 11, left associativity).

Lemma group_fact :
  ∀ (M : group) (x y : m_ty),
    x ** m_ne ** y = x ** y.
Proof.
  intros M x y.
  rewrite m_assoc. rewrite m_l_ne. reflexivity.
Qed.

EXERCISE
Give an instance of monoid for nat.

Definition nat_monoid : monoid.
Proof.
  refine {|
    m_ty := nat ;
    m_ne := 0 ;
    m_op n m := n + m
  |}.
  - intro. reflexivity.
  - intro. rewrite <- plus_n_O. reflexivity.
  - intros x y z. rewrite Nat.add_assoc. reflexivity.
Defined. (* We need Defined to access the fields! *)

Compute nat_monoid.(m_ne). (* Notation for m_neu nat_monoid *)
Check nat_monoid.(m_op).

We can prove things generically about monoids.

Notation "a ** b" := (m_op a b) (at level 11, left associativity).

EXERCISE
Prove the following fact on monoids.

Lemma monoid_fact :
  ∀ (M : monoid) (x y : M.(m_ty)),
    x ** M.(m_ne) ** y = x ** y.
Proof.
  intros M x y.
  (* More complicated than necessary of course *)
  rewrite m_assoc. rewrite m_l_ne. reflexivity.
Qed.

EXERCISE
Prove the following lemma using monoid_fact.

Lemma nat_fact :
  ∀ (x y : nat),
    x + 0 + y = x + y.
Proof.
  intros x y.
  apply monoid_fact with (M := nat_monoid).
Qed.

EXERCISE
Show that lists form a monoid using ++ as operation. How does monoid_fact translate to lists? Note that, unlike ** or +, ++ is associated to the right, meaning x ++ y ++ z stands for x ++ (y ++ z).

Definition list_monoid (A : Type) : monoid.
Proof.
  refine {|
    m_ty := list A ;
    m_ne := [] ;
    m_op x y := x ++ y
  |}.
  - intro. simpl. reflexivity.
  - intro. rewrite app_nil_r. reflexivity.
  - intros. rewrite app_assoc. reflexivity.
Defined.

Lemma list_fact :
  ∀ A (x y : list A),
    (x ++ []) ++ y = x ++ y.
Proof.
  intros A x y.
  apply monoid_fact with (M := list_monoid A).
Qed.

EXERCISE
Products of monoids also yields a monoid. Prove it.

Definition prod_monoid (M1 M2 : monoid) : monoid.
Proof.
  refine {|
    m_ty := M1.(m_ty) × M2.(m_ty) ;
    m_ne := (M1.(m_ne), M2.(m_ne)) ;
    m_op '(x,y) '(u,v) := (x ** u, y ** v)
  |}.
  - intros [x y]. rewrite !m_l_ne. reflexivity.
  - intros [x y]. rewrite !m_r_ne. reflexivity.
  - intros [x y] [u v] [a b]. rewrite !m_assoc. reflexivity.
Defined.

Classes

Class Monoid (A : Type) (neu : A) (op : A → A → A) := {
  mon_left_neutral : ∀ x, op neu x = x ;
  mon_right_neutral : ∀ x, op x neu = x ;
  mon_assoc : ∀ x y z, op (op x y) z = op x (op y z)
}.

EXERCISE
Instance is a a special command for definitions that register them as things Coq will use automatically if it has to find a value for Monoid nat 0 plus.
Don't worry too much about the export thing. This is called an attribute and it just means that if someone imports the file, then the instance will still be available. We could instead use [local] to restrict the instance to the module. It does not matter for the course. Complete the following instance. *
#[export] Instance MonoidNat : Monoid nat 0 plus.
Proof.
  split.
  - intro. reflexivity.
  - intro. lia.
  - intros. lia.
Qed.

EXERCISE
Some lemmas we can prove using only the monoid structure on (ℕ,0,+). See how Coq infers which proofs we are talking about.
Prove the following using only monoid laws.
Lemma test_nat :
  ∀ k n m, k + n + m + 0 = k + (n + m).
Proof.
  intros.
  rewrite mon_right_neutral.
  rewrite mon_assoc. reflexivity.
Qed.

EXERCISE
Prove this statement on monoids in general. Then use it to reprove it for nat.
Lemma test_monoid :
  ∀ M neu op `{Monoid M neu op} k n m,
    op (op (op k n) m) neu = op k (op n m).
Proof.
  intros.
  rewrite mon_right_neutral.
  rewrite mon_assoc. reflexivity.
Qed.

Lemma test_nat' :
  ∀ k n m, k + n + m + 0 = k + (n + m).
Proof.
  intros. apply test_monoid.
We need to give an instance of monoid for nat, but we're too lazy to find its name. It's supposed to infer it on its own! So we just give _ as the proof and Coq is fine with that.
  exact _.
Qed.

EXERCISE
Define an instance for lists and apply test_monoid to it.

#[export] Instance MonoidList : ∀ A, Monoid (list A) [] (@app A).
Proof.
  intros A.
  split.
  - intro. reflexivity.
  - intro. apply app_nil_r.
  - intros. rewrite app_assoc. reflexivity.
Qed.

Lemma test_list :
  ∀ A (k n m : list A), ((k ++ n) ++ m) ++ [] = k ++ n ++ m.
Proof.
  intros. apply test_monoid.
  exact _.
Qed.

EXERCISE
Complete the product instance.

#[export] Instance MonoidProd :
  ∀ A B na nb opa opb,
    Monoid A na opa →
    Monoid B nb opb →
    Monoid (A × B) (na,nb) (fun '(xa,xb) '(ya,yb) ⇒ (opa xa ya, opb xb yb)).
Proof.
  intros A B na nb opa opb MA MB.
  split.
  - intros [a b].
    rewrite mon_left_neutral with (x := a).
    rewrite mon_left_neutral with (x := b).
    reflexivity.
  - intros [a b].
    rewrite mon_right_neutral with (x := a).
    rewrite mon_right_neutral with (x := b).
    reflexivity.
  - intros [xa xb] [ya yb] [za zb].
    rewrite !mon_assoc. reflexivity.
Qed.

Now you can see that Coq can infer complex monoid structures on its own!
Definition foo : Monoid (list bool × nat × list nat) _ _ := _.
Print foo.

Here is another example of class: decidable equality.

Class Eq A := {
  eqb : A → A → bool ;
  eqb_iff : ∀ x y, eqb x y = true ↔ x = y
}.

EXERCISE
Complete the following function that tests whether an element is inside a list. Thanks to classes, we can define this function for all types with a decidable equality.
Give it a specification using the In predicate and show it correct with respect to it.
Note: The special tick before {Eq A} is so that we don't have to give it a name. Indeed we don't care about the name of the instance because we don't need to refer to it explicitly, Coq finds it on its own.

Fixpoint memb {A} `{Eq A} (x : A) (l : list A) : bool :=
  match l with
  | [] ⇒ false
  | y :: l ⇒ eqb x y || memb x l
  end.

Lemma memb_spec :
  ∀ A `(Eq A) (x : A) l,
    memb x l = true ↔ In x l.
Proof.
  intros A hA x l.
  induction l as [| a l ih].
  - simpl. split.
    + discriminate.
    + intros [].
  - simpl. destruct (eqb x a) eqn: e.
    + simpl. apply eqb_iff in e. subst.
      split. 2: reflexivity.
      intro. left. reflexivity.
    + simpl. split.
      × intro. right. apply ih. assumption.
      × intros [bot | h].
        1:{
          symmetry in bot. apply eqb_iff in bot. rewrite bot in e. discriminate.
        }
        apply ih. assumption.
Qed.

EXERCISE
Give an instance of Eq for nat and test memb on some lists.
You can use already proven lemmas from past weeks or from the standard library. Tip: Use the Search command as follows.

Search (nat → nat → bool).

Another useful tool is the refine attribute that also lets us give only partial instances.

#[export, refine] Instance Eq_nat : Eq nat := {|
  eqb := Nat.eqb
|}.
Proof.
  Search Nat.eqb.
  apply Nat.eqb_eq.
Defined. (* We still need to use Defined though. *)

Compute (eqb 0 1).
Compute (eqb 12 12).

Compute (memb 1 [ 3 ; 5 ; 1 ]).
Compute (memb 12 [ 3 ; 5 ; 1 ]).

EXERCISE
Define a class of groups and show uniqueness of neutral and inverse for all group.
Apply this result to a group of your choosing (you will have to provide an instance). To apply a lemma, sometimes apply is not enough. In this case you can use eapply which is more permissive. It creates existential variables (starting with a question mark) corresponding to values it couldn't guess. They are typically resolved as you prove the various goals.
Can you show that every group forms a monoid (again, provide a generic instance)?

Class Group A (ne : A) (op : A → A → A) := {
  group_left_neutral : ∀ x, op ne x = x ;
  group_right_neutral : ∀ x, op x ne = x ;
  group_assoc : ∀ x y z, op (op x y) z = op x (op y z) ;
  group_inv : ∀ x, ∃ y, op x y = ne ∧ op y x = ne
}.

Lemma group_neutral_unique :
  ∀ G ne op `{Group G ne op} ne',
    (∀ x, op ne' x = x) →
    (∀ x, op x ne' = x) →
    ne = ne'.
Proof.
  intros G ne op H ne' hl hr.
  specialize (hl ne). rewrite group_right_neutral in hl. subst.
  reflexivity.
Qed.

Lemma group_inverse_unique :
  ∀ G ne op `{Group G ne op} a b c,
    op a b = ne →
    op b a = ne →
    op a c = ne →
    op c a = ne →
    b = c.
Proof.
  intros G ne op H a b c hbr hbl hcr hcl.
  apply (f_equal (op c)) in hbr.
  rewrite <- group_assoc in hbr. rewrite hcl in hbr.
  rewrite group_left_neutral in hbr.
  rewrite group_right_neutral in hbr. assumption.
Qed.

#[export] Instance Group_Z : Group Z 0%Z Z.add.
Proof.
  constructor.
  - intro. lia.
  - intro. lia.
  - intros. lia.
  - intro x. ∃ (- x)%Z. lia.
Qed.

Lemma one_zero_Z :
  ∀ (z : Z),
    (∀ i, z + i = i)%Z →
    (∀ i, i + z = i)%Z →
    z = 0%Z.
Proof.
  intros z hl hr.
  symmetry.
  eapply group_neutral_unique. 1: exact _.
  all: assumption.
Qed.

#[export] Instance Monoid_Group :
  ∀ G ne op,
    Group G ne op →
    Monoid G ne op.
Proof.
  intros G ne op H.
  constructor.
  - intro. apply group_left_neutral.
  - intro. apply group_right_neutral.
  - intros x y z. apply group_assoc.
Qed.

AUTOMATION
Classes are one form of automation. There are others in Coq. The main one being tactics. Indeed they can be used to derive properties automatically. We will start by looking again at the In predicate.
We'll start by proving some easy lemmas.
EXERCISE
Prove the following lemmas using auto to conclude.

Lemma In_hd :
  ∀ A (x : A) l,
    In x (x :: l).
Proof.
  intros A x l.
  simpl. auto.
Qed.

Lemma In_tl :
  ∀ A (x y : A) l,
    In x l →
    In x (y :: l).
Proof.
  intros A x y l h.
  simpl. auto.
Qed.

EXERCISE
Now we would like auto to deal with In without the need to use simpl. It should also be able to deal with more complex examples like the following.
Prove it by hand first.

Lemma In_4 :
  ∀ A (x a b c d : A) l,
    In x l →
    In x (a :: b :: c :: d :: l).
Proof.
  intros A x a b c d l h.
  auto. (* You can see it does nothing. *)
  apply In_tl. apply In_tl. (* This is annoying let's use repeat: *)
  repeat apply In_tl.
  auto.
Abort. (* We don't need this lemma, so I abort in order not to save it. *)

Applying the lemma by hand is not very nice, and rather tedious. We're going to declare hints so that auto knows how to use them.
In fact, we're first going to declare a new database of hints dedicated to In. We call it indb, because why not?

Create HintDb indb.

We then add hints to the database using the Hint Resolve command. Like for instances, we need to specify a locality. It doesn't matter so we're going to go with export as before. We then give it the name of a definition (or lemma etc.) and after the colon the databases to which we want to add the hint.

#[export] Hint Resolve In_hd : indb.

EXERCISE
Prove the following lemma with auto.

Lemma In_hd' :
  ∀ A (x : A) l,
    In x (x :: l).
Proof.
  intros A x l.
  auto. (* It still doesn't work, because auto doesn't use indb by default. *)
  auto with indb. (* Now it does! *)
Restart.
  auto with indb.
Qed.

EXERCISE
Expand the database so that auto with indb is enough to solve the following goals.
Note: Goal is like Lemma but it doesn't require a name. You won't be able to reuse the proven goal afterwards, but it's useful to test things.

#[export] Hint Resolve In_tl : indb.

Goal ∀ A (x a b c d : A) l,
  In x l →
  In x (a :: b :: c :: d :: l).
Proof.
  auto with indb.
Qed.

Goal ∀ A (x a b c d : A) l,
  In x (a :: b :: x :: c :: d :: l).
Proof.
  auto with indb.
Qed.

EXERCISE
Show that In x l implies In x (l ++ r) and that In x r implies In x (l ++ r).

Lemma In_app_l :
  ∀ A (x : A) l r,
    In x l →
    In x (l ++ r).
Proof.
  intros A x l r h.
  induction l as [| y l ih] in r, h |- ×.
  - simpl in h. contradiction.
  - simpl. simpl in h. destruct h as [h | h].
    + left. assumption.
    + right. apply ih. assumption.
Qed.

Lemma In_app_r :
  ∀ A (x : A) l r,
    In x r →
    In x (l ++ r).
Proof.
  intros A x l r h.
  induction l as [| y l ih] in r, h |- ×.
  - simpl. assumption.
  - simpl. right. apply ih. assumption.
Qed.

EXERCISE
Now add both lemmas to indb, for the first time we are introducing a choice for auto: presented with the goal In x (l ++ r) it has to choose whether to go left or right. It has no way to know in advance which one is better so it will pick one and backtrack if it doesn't work.
Use it to solve the two following goals.

#[export] Hint Resolve In_app_l : indb.
#[export] Hint Resolve In_app_r : indb.

Goal ∀ A (x a b c d : A) l l',
  In x l →
  In x ([ a ; b ; c ] ++ l' ++ d :: l).
Proof.
  auto with indb.
Qed.

Goal ∀ A (x a b c d : A) l l',
  In x l →
  In x (l ++ [ a ; b ; c ] ++ l' ++ [ d ]).
Proof.
  auto with indb.
Qed.

EXERCISE
What if the element in my list is not syntactically what I'm looking for but only equal to it?
Prove a lemma for this particular case and add a hint for it. It should solve the following goal.

Lemma In_hd_eq :
  ∀ A (x y : A) l,
    x = y →
    In x (y :: l).
Proof.
  intros A x l.
  simpl. auto.
Qed.

#[export] Hint Resolve In_hd_eq : indb.

Goal ∀ A (x y a b c d : A) l l',
  x = y →
  In x ([ a ; b ; c ] ++ l' ++ d :: y :: l).
Proof.
  auto with indb.
Qed.

EXERCISE
This equality is not always going to be an assumption in the context. But it could be handled by some more automation. There is for instance the arith database that can deal with arithmetic.
You can give two (or more) databases to auto. Check that it indeed succeeds in the following goal with arith but not without.

Goal ∀ (a b c d : nat) l l',
  In (a + b) ([ b ; c ] ++ l' ++ d :: (b + a) :: l).
Proof.
  auto with indb.
  auto with indb arith.
Qed.

EXERCISE
Sadly, it has its limits, check that it isn't sufficient for the following goal even though you should be able to prove it (do it).
Hint: lia is stronger than auto with arith on that one.

Goal ∀ (a b c d : nat) l l',
  In (a + b + c) ([ a ; b ; c ] ++ l' ++ d :: (c + 0 + a + b) :: l).
Proof.
  intros.
  auto with indb arith.
  repeat apply In_tl.
  apply In_app_r. apply In_tl. apply In_hd_eq.
  lia.
Qed.

ADVANCED EXERCISE
There is a way to use lia with auto actually. For this we have to provide a different kind of hint. Using the command Hint Extern we can tell Coq what tactic to try when encountering a goal of the form n = m where n, m : nat.
Below what we do is say that when the goal is of the shape @eq nat _ then we apply lia. We add this to indb. The 3 is something called cost. auto is acutally cost-based and each action it takes has a cost attached to it. auto will start by picking the actions with the lowest cost when it has a choice. When it runs out of money, it gives up.
Check that you can solve the previous goal using auto with indb. Can you also make it so that the other goal works?

#[export] Hint Extern 3 (@eq nat _ _) ⇒ lia : indb.

Goal ∀ (a b c d : nat) l l',
  In (a + b + c) ([ a ; b ; c ] ++ l' ++ d :: (c + 0 + a + b) :: l).
Proof.
  auto with indb.
Qed.

#[export] Hint Extern 3 (@eq Z _ _) ⇒ lia : indb.

Goal ∀ (a b c d : Z) l l',
  In (a + b + c)%Z ([ a ; b ; c ] ++ l' ++ d :: (c + d + 0 + a - d + b) :: l)%Z.
Proof.
  auto with indb.
Qed.

Existential variables
We have hinted at eapply already. But many tactics come with an e version. One such example is the eexists tactic that is very convenient. See below.

Goal ∀ n, n = 0 ∨ ∃ m, n = S m.
Proof.
  intro n.
  destruct n.
  - auto.
  - right. eexists. reflexivity.
  (* We're going to show the proof to see what auto picked for a value *)
  Show Proof.
Qed.

EXERCISE
Solve the following goal without using any lemma or variable in the context explicitly.

Goal ∀ A (x : A) l l',
  ∃ y, In y (l ++ x :: l').
Proof.
  intros.
  eexists.
  auto with indb.
Qed.

auto also has an eauto variant. You can use it to deal with quantifiers. It is generally slower than auto so you can use it when auto fails.

Goal ∀ (P : nat → nat → Prop) (Q : nat → Prop),
  P 4 2 →
  (∀ x y, P x y → Q x) →
  Q 4.
Proof.
  intros P Q hP h.
  apply h with (y := 2). assumption.
Restart.
  intros P Q hP h.
  eapply h.
  eassumption. (* Notice how we need the e here too! *)
Restart.
  eauto.
Qed.

EXERCISE
Solve the following goal.

Goal ∀ A (P : A → A → Prop) (Q : A → Prop),
  (∀ x, ∃ y, P x y) →
  (∀ x y, P x y → Q x) →
  (∀ x, Q x).
Proof.
  intros A P Q h1 h2 x.
  specialize (h1 x) as [y h1].
  eauto.
Qed.

ADVANCED: SETOID REWRITE
Another interesting feature of Coq is the ability to rewrite on other things rather than just equality.
For instance, we can use rewrite for logical equivalences. Let us go through it step by step.
EXERCISE
To begin, prove the following logical equivalences.

Lemma and_AA :
  ∀ A, A ∧ A ↔ A.
Proof.
  intro A. split.
  - intros []. auto.
  - auto.
Qed.

Lemma or_AA :
  ∀ A, A ∨ A ↔ A.
Proof.
  intro A. split.
  - intros []. all: auto.
  - auto.
Qed.

Lemma and_com :
  ∀ A B,
    A ∧ B ↔ B ∧ A.
Proof.
  intros A B. split.
  all: intros [] ; auto.
Qed.

Lemma or_com :
  ∀ A B,
    A ∨ B ↔ B ∨ A.
Proof.
  intros A B. split.
  all: intros [] ; auto.
Qed.

Lemma and_assoc :
  ∀ A B C,
    (A ∧ B) ∧ C ↔ A ∧ B ∧ C.
Proof.
  intros A B C. split.
  - intros [[] ?]. auto.
  - intros [? []]. auto.
Qed.

EXERCISE
Now you can solve the following goals just by using rewrite on equivalences. No more need for split!
Note that you can also use reflexivity, symmetry and transitivity on those. Under the hood, this is using class resolution to find the proper instances. For iff (logical equivalence) they are already registered so we can freely use them.

Goal ∀ (A B C D : Prop),
  A ∧ (B ∧ B) ∧ (C → D) ∧ (C → D) ↔ A ∧ B ∧ (C → D).
Proof.
  intros A B C D.
  rewrite !and_AA.
  reflexivity.
Qed.

Goal ∀ (A B : Prop),
  (B ∧ A ∧ B) ∨ (A ∧ B) ↔ B ∧ A.
Proof.
  intros A B.
  rewrite (and_com A B). rewrite <- and_assoc. rewrite and_AA.
  rewrite or_AA.
  reflexivity.
Qed.

EXERCISE
Ok, this is getting old. We're going to switch to another notion which isn't already registered in the standard library. First we're going to introduce a relation on lists that relates two lists if they have the same elements (regardless of how many times they appear), ie if they represent the same set.
Complete the following definition.

Definition list_set_eq {A} (u v : list A) : Prop :=
  ∀ x, In x u ↔ In x v.

Notation "u ~ v" := (list_set_eq u v) (at level 70).

EXERCISE
We first need to show that the relation is reflexive, symmetric and transitive. We do so by instantiating the right classes so that we can use the corresponding tactics (as for iff).
Check it works with the provided goal.

From Coq Require Import Setoid.

#[export] Instance list_set_eq_refl :
  ∀ A, Reflexive (list_set_eq (A := A)).
Proof.
  intro A. intro l. intro x. reflexivity.
Qed.

#[export] Instance list_set_eq_sym :
  ∀ A, Symmetric (list_set_eq (A := A)).
Proof.
  intro A. intros u v h.
  intro x. symmetry. apply h.
Qed.

#[export] Instance list_set_eq_trans :
  ∀ A, Transitive (list_set_eq (A := A)).
Proof.
  intro A. intros u v w h1 h2.
  intro x. etransitivity.
  - eapply h1.
  - apply h2.
Qed.

Goal ∀ A (u v w : list A),
  v ¬ u →
  (u ¬ u → v ¬ w) →
  u ¬ w.
Proof.
  intros A u v w h1 h2.
  etransitivity.
  - symmetry. eassumption.
  - eapply h2. reflexivity.
Qed.

EXERCISE
Prove the following goal using rewrite. This is just transitivity again but this is to show you how it works on a simple example.

Goal ∀ A (u v w : list A),
  u ¬ v →
  v ¬ w →
  u ¬ w.
Proof.
  intros A u v w h1 h2.
  rewrite h1. assumption.
Qed.

EXERCISE
Prove that u ++ v ~ v ++ u.

Lemma In_app_inv :
  ∀ A (l r : list A) x,
    In x (l ++ r) →
    In x l ∨ In x r.
Proof.
  intros A l r x h.
  induction l as [| a l ih] in r, h |- ×.
  - simpl in ×. auto.
  - simpl in ×. destruct h as [h | h].
    + eauto with indb.
    + specialize ih with (1 := h). destruct ih.
      all: auto with indb.
Qed.

Lemma list_seq_eq_app :
  ∀ A (u v : list A),
    u ++ v ¬ v ++ u.
Proof.
  intros A u v. intro x. split.
  all: intros h%In_app_inv. all: destruct h.
  all: auto with indb.
Qed.

EXERCISE
In order to rewrite this relation inside, eg., In, we have to first show that In is invariant by ~. In other words that u ~ v implies In x u <-> In x v. We can use the following command to declare it. This will in turn let us rewrite inside In.
Prove that we indeed have a morpshim. Prove the given goals using rewrite.

Add Parametric Morphism A (x : A) : (In x)
  with signature list_set_eq ==> iff
  as In_morph.
Proof.
  intros u v e. apply e.
Qed.

Goal ∀ A (x : A) u v,
  In x (u ++ v) →
  In x (v ++ u).
Proof.
  intros A x u v h.
  rewrite list_seq_eq_app. assumption.
Qed.

Goal ∀ A (x a b c : A) u v,
  In x (u ++ [ a ; b ; c ] ++ x :: v).
Proof.
  intros A x a b c u v.
  rewrite list_seq_eq_app.
  rewrite <- app_assoc.
  rewrite list_seq_eq_app.
  rewrite <- app_assoc. simpl. auto.
Qed.

EXERCISE
Look up the Forall predicate. Show that it is a morphism for list_set_eq. Proceed to solve the following goal.

Lemma Forall_In :
  ∀ A (P : A → Prop) l,
    Forall P l ↔ (∀ x, In x l → P x).
Proof.
  intros A P l.
  induction l as [| x l ih].
  - split.
    + simpl. intros _ _ [].
    + intros _. constructor.
  - split.
    + intros h a ha.
      inversion h. subst.
      simpl in ha. destruct ha as [e | hl].
      × subst. assumption.
      × apply ih. all: assumption.
    + intro h. constructor.
      × apply h. auto with indb.
      × rewrite ih. intros a ha.
        apply h. auto with indb.
Qed.

Lemma Forall_set_eq :
  ∀ A (P : A → Prop) u v,
    u ¬ v →
    Forall P u →
    Forall P v.
Proof.
  intros A P u v e h.
  rewrite Forall_In in h |- ×.
  intros x hx.
  rewrite <- e in hx.
  apply h. assumption.
Qed.

Add Parametric Morphism A P : (@Forall A P)
  with signature list_set_eq ==> iff
  as Forall_morph.
Proof.
  intros u v e.
  split. all: apply Forall_set_eq.
  - auto.
  - symmetry. auto.
Qed.

Goal ∀ u v w,
  let P n := ∃ m, n = 2 × m in
  Forall P (w ++ u ++ v) →
  Forall P (u ++ v ++ w).
Proof.
  intros u v w P h.
  rewrite list_seq_eq_app.
  rewrite <- app_assoc.
  rewrite list_seq_eq_app.
  rewrite <- app_assoc.
  assumption.
Qed.