(** * Large discrimination and inversion *)

(** ** Context *)

(** Our favorite colors *)
Inductive color : Set :=
| Purple : color
| Indigo : color
| Blue : color
| Green : color
| Yellow : color
| Orange : color
| Red : color
.

Inductive nextcolor : color -> color -> Prop :=
| NCg : nextcolor Green Orange
| NCo : nextcolor Orange Red
| NCr : nextcolor Red Green
.

(* ====================================================================== *)
(** ** Discrimination *)

(** Seen before: contagious equalities *)
Lemma discrim_Green_Orange :
  Green = Orange -> forall {X: Set}, forall x y: X, x = y.
Proof.
  intros e X x y.
  pose (f c := match c with Green => x | _  => y end).
  change x with (f Green). rewrite e. cbn. reflexivity.
Qed.

(** Super-contagious equalities.
    We can even go further, that is, prove anything
    from such an equality.
    Idea : rewrite no longer on a value, but on a
    proposition.
    In the case we will replace [P] by a proven proposition.
    Here we take hypothesis [e], but
    [0 = 0] does the job as well.
    Remark:
    we have a change of "floor" in the building of values and types.
    This was already used in the [waow] function, with [Set] instead
    of [Prop]. This feature is called "large elimination".
 *)
(** Warning, here we consider [Red = Orange] *)
Lemma discrim_Red_Orange_large :
  Red = Orange -> forall P: Prop, P.
Proof.
  intros e P.
  pose (f c := match c with Red => P | _  => Red = Orange end).
  change (f Red). rewrite e. cbv. exact e.
Qed.

(** Variant with [0 = 0] *)
Lemma discrim_Red_Orange_large_using_0_eq_0 :
  Red = Orange -> forall P: Prop, P.
Proof.
  intros e P.
  pose (f c := match c with Red => P | _  => 0 = 0 end).
  change (f Red). rewrite e. cbv. reflexivity.
Qed.

(** **** Tactic discriminate *)
(** Coq includes tactic [discriminate], based on a similar program. *)
Lemma discrim_Red_Orange_large_with_discriminate :
  Red = Orange -> forall P: Prop, P.
Proof.
  intros e P. discriminate e.
Qed.

(** Tactic [discriminate] works as soon as we have an hypothesis
    stating that two expressions starting with two different constructors
    are equal. *)

(* ====================================================================== *)
(** ** Inversion *)

(** *** Hidden subtleties of [destruct] *)

(** **** Tactic [revert] *)
(** **** Tactic combinator [try] *)
(** We start with the following lemma *)
Lemma Red_follows_Orange :
  forall c1 c2 : color, c1 = Orange -> nextcolor c1 c2 -> c2 = Red.
  intros c1 c2 e1 nc.

  (** Step 1:  by case on [nc] *)
  (** This yields for [c1] and [c2], respectively
      - Green and Orange,
      - Orange and Red,
      - Red and Green.
      Observe that [c1] is used in [e1].  To clarify what happens,
      a nice thing to do is to put [e1] in the conclusion.
      To this effect we perform an "intro upside down",
      eitehr with an appropriate [refine]... *)
  refine ( (_ : c1 = Orange -> c2 = Red) e1); clear e1.
  Undo 1.
  (** ... or with tactic [revert], that performs this [refine] *)
  revert e1.

  (** Equality [c1 = Orange] palys the rôle of a Trojan horse:
      the case analysis on [nc] inserts a useful information
      in the subgoals corresponding to the subcases. *)

  (** To clearly understand the reasoning by case in [nc],
      we use [refine] (optionally followed by [clear]).
      For example in the first case, [c1] and [c2] are respectively
      [Green] and [Orange], that can be made explicite in the script. *)
  refine (match nc with
          | NCg => _ : Green = Orange -> Orange = Red
          | NCo => _
          | NCr => _
          end); clear.
  (** As an [intro e1] will be performed in each case, let us factor... *)
  Undo 1.
  (** ... and use [destruct], shorter here than the equivalent pattern matching. *)
  destruct nc as [ | | ]; intro e1.

  (** Actually, tactic [destruct] performs a lot of work:
      - looking for hypotheses affected by [nc]
      - reverting those hypotheses
      - [refine (match ... end)],      HERE IS THE CORE
        followed by [clear]
      - reintroduction of the hypotheses coming from [revert]
      Finally, all logical subtleties of step 1 are performed
      within a single invocation of [destruct]!
 *)
  Undo 2.
  destruct nc as [ | | ].

  (** Step 2:  finish using discrimination and reflexivity *)
  - (* usual contagious equality *)
    rewrite (discrim_Green_Orange e1 Orange Red). reflexivity.
  - reflexivity.
  - (* "large contagious equality *)
    apply (discrim_Red_Orange_large e1).
    (** Or with tactic [discriminate] *)
    Undo 1.
    discriminate e1.

  (** Let us summarize using a very short script;
      note the use of [try] to evacuate all contagious cases,
      leaving only the relevant case where [c1] is [Red]. *)
  Restart.

  intros c1 c2 e1 nc.
  destruct nc as [ | | ]; try discriminate e1.
  reflexivity.
Qed.


(** Take-home lessons learned from the above:
- from now on, we can evacuate "absurd" goals coming
  from a contagious equality in hypothesis using
  [discriminate] (or better: [try discriminate]);
- the work done by [destruct] is remarkable;
  a manual proof where all steps are explicit should
  show all all these details!
- to keep in mind: [induction] does a similar work;
- it is often convenient but sometimes dangerous:
  we saw that some goals need a preliminary cleaning
  using tactic [clear] because otherwise, undesired
  parasitic Trojan horses could weaken induction
  hypotheses so that they become unusable.
 *)

(** After this god news on [destruct], one could believe
    that [destruct] works as expected in all situations.
    However, here is an attempt that will fail.
    We try to sho a variant of the above lemma,
    expressed in a shorter way, without the intermediary
    equality [c1 = Orange]. *)
(** We come back to [Red_follows_Orange] *)

Theorem Red_follows_Orange_short :
  forall c2, nextcolor Orange c2 -> c2 = Red.
Proof.
  intros c2 nc.
  destruct nc as [ | | ].
  (** Here we are stuck. *)
Abort.

(** In order to understand let us start with a first observation.
    We define two functions on natural numbers.
 *)

Definition func1 (n : nat) :=
  match n with
  | O => Green
  | S p => Red
  end.

Definition func2 (n : nat) :=
  match n with
  | O => Orange
  | S p => Green
  end.

(** And let us show the following lemma *)
Example prelim_destruct :
  forall n m, nextcolor (func1 (n+3*m)) (func2 (n+3*m)).
Proof.
  intros n m.
  (** We resaon by case on expression [n+3*m], which is
      - either [0]
      - or [S p]  *)
  refine (match n+3*m with O => _ | S p => _ end). Undo 1.
  (** look carefully at the goals obtained *)
  destruct (n+3*m) as [ | p].
  - cbv. apply NCg.
  - cbv. apply NCr.
Qed.

(** The point is that the case analysis was done
    without taking into account that originally, [O] ou [S p] was [n+3*m].
    It can be seen because it is a simple [destruct] that can as well
    be written with [refine-match] :
    refine (match n+3*m with O => _ | S p => _ end).
    In such a program, the identity between [n+3*m] and [O] (or [S p])
    disappears naturally. *)

(** Same observation if the expression is given by a constructor *)
Example prelim_destruct_zero :
  nextcolor (func1 0) (func2 0).
Proof.
  cbv.
  (** Of course [apply NCg] will work but this is not the point, we
      want to observe what happens if we try a case analysis.
      And [destruct] (or the underluing pattern-matching) behaves
      exactly as in [prelim_destruct] *)
  Undo 1.
  destruct O as [ | p].
  - cbv. apply NCg.
  - cbv. apply NCr.
Qed.

(** We come back to [Red_follows_Orange] *)
Theorem Red_follows_Orange_short :
  forall c2, nextcolor Orange c2 -> c2 = Red.
Proof.
  intros c2 nc.
  destruct nc as [ | | ].
  (** Here we are stuck. *)
  Undo 1.
  (*  Similarly, the underlying [match nc ... end] just
      identifies the 2 arguments of [nc] with, respectively:
      - [Green] and [Orange],
      - [Orange] and [Red],
      - [Red] and [Green],
      even if one of those arguments is already [Orange].
      It is frustrating but just NORMAL!
      It is consistent with the behaviour explained on
      [prelim_destruct_zero].
   *)
  (** In order to make [destruct nc] work as expected, it is then necessary
      to replace the argument fixed to be [Orange] by a variable or,
      intuitively, to detach this information and put it in a
      Trojan horse.  In other words, we want to retrieve the situation
      of lemma [Red_follows_Orange].
      To this effect we introduce a suitable Lemma called [souvenir]. *)
Abort.

(** A lemma to be used to build a Trohan horse, i.e.,
    a new variable equal to [Orange]. *)
Lemma souvenir_Orange :
  forall (P : color -> Prop),
    (forall c, c = Orange -> P c) -> P Orange.
Proof.
  intros P aj_eg.
  apply aj_eg.
  reflexivity.
Qed.

(** General version, with [y : X] instead of the specific [Orange : color]. *)
Lemma souvenir :
  forall {X: Set} (y : X) (P : X -> Prop),
    (forall x, x = y -> P x) -> P y.
Proof.
  intros X y P aj_eg.
  apply aj_eg.
  reflexivity.
Qed.

(** **** Tactic [pattern] *)
Example prelim_destruct_souvenir :
  forall n m, nextcolor (func1 (n+3*m)) (func2 (n+3*m)).
Proof.
  intros n m.
  (** Replacing [n+3*m] by a variable [n3m] and an
      equality [e : n3m = n + 3*m].  *)
  (** We first make the predicate [P] explicit *)
  change ((fun n3m => nextcolor (func1 n3m) (func2 n3m)) (n + 3 * m)).
  (** This [change] can be done with the conversion tactic [pattern] *)
  Undo 1.
  pattern (n + 3 * m).
  apply souvenir. intros n3m e.
  destruct n3m as [ | p]; cbv.
  - apply NCg.
  - apply NCr.
Qed.

(** Coq provides a tactic with a similar effect.
    Note that this tactic can be used in one of the exercises
    on the natural semantics of languages WHILE and REPEAT.
 *)
(** **** Tactic case_eq *)
Example prelim_destruct_case_eq :
  forall n m, nextcolor (func1 (n+3*m)) (func2 (n+3*m)).
Proof.
  intros n m.
  case_eq (n+3*m).
  - intros e. apply NCg.
  - intros p e. apply NCr.
Qed.

(** Let us use [pattern] and [souvenir] on [nextcolor Orange c2] *)

Theorem Red_follows_Orange_short :
  forall c2, nextcolor Orange c2 -> c2 = Red.
Proof.
  intro c2.
  (** Step 1: replace Orange by a variable [c1] and an
      equality [e1 : c1 = Orange]. *)
  pattern Orange. apply souvenir.
  intros c1 e1 nc.

  (** Step 2: as in [Red_follows_Orange] *)
  destruct nc as [ | | ]; try discriminate e1.
  reflexivity.
Qed.

(** Essential observation: hypothesis [nc : nextcolor Orange c2]
    contains TWO simultaneous constraints:
    - the proof-tree referred to by [nc] has a priori one of
      three forms indicated by constructors [NCg], [NCo] and [NCr]
      (which entails that the corresponding arguments of [nextcolor]
      are respectively either [Green] and [Orange], or [Orange] and [Red],
      or [Red] and [Green]) ;
    - the first argument of [nextcolor] is actually [Orange];
      but here, the first argument of [NCg], [NCo] and [NCr] is always
      a constructor (the second argument as well but it is irrelevant
      here).
    It is the combination of these two constraints that, finally, restricts
    the actual number of possible cases for [nc] to only one, [Cso], because
    the others force [Orange] to be equal to [Green] or to [Red].
    To get this with [destruct nc] we must first prepare the ground
    with lemma [souvenir] then clean the irrelevant cases
    with [discriminate].

    The combination hypothesis in an inductive type + argument
    fixed to be a constructor is common.
    To deal with it, Coq includes tactic [inversion],
    that does a job equivalent to what is explained above.
*)

(** **** Tactic inversion *)
Theorem Red_follows_Orange_short_with_inversion :
  forall c2, nextcolor Orange c2 -> c2 = Red.
Proof.
  intros c2 nc. inversion nc. reflexivity.
Qed.

(* ---------------------------------------------------------------------- *)
(** **** And if the color has no following color? *)

(** If a color follows Purple, it's party. *)
Theorem nothing_follows_Purple :
  forall c2, nextcolor Purple c2 -> forall P: Prop, P.
Proof.
  intros c2 nc P.
  (** Tactic [inversion] immediatly solves the goal. *)
  inversion nc.
  (** But let us try to understand, using the previous technique. *)
  Undo 1.
  revert nc. pattern Purple. apply souvenir. intros c1 e1 nc.
  (** The following is too simple, no effect on [e1] *)
  refine (match nc with
          | NCg =>  _
          | NCo =>  _
          | NCr =>  _
          end).
  Undo 1.
  (** So [e1] needs to be put in the conclusion first (Trojan horse) *)
  revert e1.
  (** Each subgoal will start with an [intro e1], or a [fun] *)
  refine (match nc with
          | NCg => fun e1 => _
          | NCo => fun e1 => _
          | NCr => fun e1 => _
          end).
  (** At this stage, in the 3 possible cases for [nc], [c1] can be [Green],
      [Orange] or [Red];
      equality [e1] becomes super-contagious and can be exploited
      using [discriminate]. *)
  (** Let us restart with [destruct] which silently performs the [revert]
      and the [intro]. *)
  Undo 2.
  destruct nc as [ | | ].
  - discriminate.
  - discriminate.
  - discriminate.
Qed.

(* ---------------------------------------------------------------------- *)
(** A more interesting example *)
(** **** Tactic [subst] *)
Theorem nextcolor3 :
  forall c1 c2 c3 c4,
    nextcolor c1 c2 ->
    nextcolor c2 c3 ->
    nextcolor c3 c4 ->
    c4 = c1.
Proof.
  intros c1 c2 c3 c4 nc1 nc2 nc3.
  destruct nc1 as [ | | ].
  - inversion nc2.
    (** Tactic [inversion] tends to introduce equalities
        that are often better to be systematically used to
        clean the goal. Tactic [subst] does this job. *)
    subst.
    inversion nc3.
    reflexivity.
  - (** We see that all sub-goals can be solved in the same way,
        so a single series of tactinc will work at once. *)
  Restart.

  intros c1 c2 c3 c4 nc1 nc2 nc3.
  destruct nc1 as [ | | ];
  inversion nc2; subst; inversion nc3; reflexivity.
Qed.

Print nextcolor3.