(** * Small inversions *)

Inductive color : Set :=
| Purple : color
| Indigo : color
| Blue : color
| Green : color
| Yellow : color
| Orange : color
| Red : color
.

(** We saw how to perform inversions using lemma [souvenir] and
    repeated uses of [discriminate].
    All of the latter proceed by case analysis on the
    "piloting argument" [c1] in
    [nc : nextcolor c1 c2].
    Here is a more elegant technique, where the case analysis
    on [c1] is done only once.

    We compute a predicate for each constructor of [color],
    corresponding to a "slice"  of the relation [nextcolor]
    when its "driving argument" (pilot for short) is fixed
    to be a given color.

    Here we choose the first argument as the pilot.
 *)

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

(** Predicates corresponding to partial versions of [nextcolor]
    when the pilot is fixed. *)
Inductive nextcolor_Green : color -> Prop :=
| NCg' : nextcolor_Green Orange.

Inductive nextcolor_Orange : color -> Prop :=
| NCo' : nextcolor_Orange Red.

Inductive nextcolor_Red : color -> Prop :=
| NCr' : nextcolor_Red Green.

(** For remaining colors there is no constructor. *)
Inductive nextcolor_no : color -> Prop := .

(** For each value of the pilot we return one of
    the above predicates. *)
Definition nextcolor_dispatch (c: color) : color -> Prop :=
  match c with
  | Green  => nextcolor_Green
  | Orange => nextcolor_Orange
  | Red    => nextcolor_Red
  | _      => nextcolor_no
  end.

(** From [nc : nextcolor c1 c2], we infer the relevant partial
    predicate according to [c1]: either [nextcolor_Green], or
    [nextcolor_Orange], etc.  *)
Definition nextcolor_inv {c1 c2}
  (nc : nextcolor c1 c2) : nextcolor_dispatch c1 c2.
Proof. destruct nc as [ | | ]; cbn; constructor. Qed.

Print nextcolor_inv.
Reset nextcolor_inv.

(** Explicit and readable version *)
Definition nextcolor_inv {c1 c2}
  (nc : nextcolor c1 c2) : nextcolor_dispatch c1 c2 :=
  match nc with
  | NCg => NCg'
  | NCo => NCo'
  | NCr => NCr'
  end.

(** Usage : in order to "invert", say, [nc : nextcolor Green x],
    instead of reasoning by case on [nc], we reason by case on
    [nextcolor_inv nc], of type [nextcolor_Green], that contains
    only one constructor [NCg'] build on the same model as [NCg];
    it is like a [destruct nc] where only the relevant
    cases are left.
 *)

Theorem nextcolor3_smallinv :
  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.
  (** Il y a 3 cas pour nc1 *)
  destruct nc1 as [ | | ].
  - Check (nextcolor_inv nc2 : nextcolor_Orange c3).
    (** Advantage of this technique: no parasitic equality is generated:
        the only possible proof of [nextcolor_Orange c3) constrains
        [c3] to be [Red], which is propagated in the goal obtained *)
    destruct (nextcolor_inv nc2).
    (** Same for [nc3] that constrains [c4] to be [Green] *)
    destruct (nextcolor_inv nc3).
    reflexivity.
    (** Using the same sequence of tactinc in each case for [nc1]. *)
    Restart.

  intros c1 c2 c3 c4 nc1 nc2 nc3.
  destruct nc1 as [ | | ];
  destruct (nextcolor_inv nc2);
  destruct (nextcolor_inv nc3);
  reflexivity.
Qed.

(** For [Purple], [nextcolor_inv nc] is of type [nextcolor_no c2]
    with no constructor; then the case analysis provides 0 cases,
    and then no subgoal: the proof is finished. *)
Theorem nothing_follows_Purple :
  forall c2, nextcolor Purple c2 -> forall P: Prop, P.
Proof.
  intros c2 nc P.
  Check (nextcolor_inv nc : nextcolor_no c2).
  (** No color follows [Purple], then zero case to be considered. *)
  destruct (nextcolor_inv nc).
  (** Still easier to see with an explicit pattern matching *)
  Undo 1.
  refine (match nextcolor_inv nc with end).
Qed.

(* ------------------------------------------------------------------ *)
(** A more complex example: yet another next color *)


(**

  Blue --> Indigo --> Purple
                  \
                   +--> d such that Yellow --> c  and  c ==> d
                                (then dead branch)

  Yellow -----+
     ^       /
      \--<--+

  Green --> Orange --> Red +
   ^                       /
    \---------<-----------+

 *)


Inductive yanextcolor : color -> color -> Prop :=
| YNCb  : yanextcolor Blue Indigo
| YNCi1 : yanextcolor Indigo Purple
| YNCi2 : forall c d,
    yanextcolor Yellow c -> nextcolor c d -> yanextcolor Indigo c
| YNCy  : yanextcolor Yellow Yellow
| YNCg  : yanextcolor Green Orange
| YNCo  : yanextcolor Orange Red
| YNCr  : yanextcolor Red Green
.

(** Theorem yanextcolor3 can be proved,
    with more cases to be considerered. *)

(** Using standard inversion first *)
Theorem yanextcolor3_stdinv :
  forall c1 c2 c3 c4,
    yanextcolor c1 c2 ->
    yanextcolor c2 c3 ->
    yanextcolor c3 c4 ->
    c4 = c1.
Proof.
  intros c1 c2 c3 c4 ync1 ync2 ync3.
  destruct ync1 as [ | | c d ync1' nc | | | | ].
  - inversion ync2; subst.
    + inversion ync3.
    + inversion H; subst. inversion H0.
  - inversion ync2.
  - inversion ync1'; subst. inversion nc.
  - inversion ync2; subst; inversion ync3; reflexivity.
  - inversion ync2; subst; inversion ync3; reflexivity.
  - inversion ync2; subst; inversion ync3; reflexivity.
  - inversion ync2; subst; inversion ync3; reflexivity.
Qed.

Print yanextcolor3_stdinv. (** > 900 lines *)

(* --------------------------- *)
(** Small inversions *)

(** Partial predicates. *)
(** Indigo has two constructors *)
Inductive yanextcolor_Blue : color -> Prop :=
| YNCb'  : yanextcolor_Blue Indigo.

Inductive yanextcolor_Indigo : color -> Prop :=
| YNCi1' : yanextcolor_Indigo Purple
| YNCi2' : forall c d,
    yanextcolor Yellow c -> nextcolor c d -> yanextcolor_Indigo c.

Inductive yanextcolor_Yellow : color -> Prop :=
| YNCy'  : yanextcolor_Yellow Yellow.

Inductive yanextcolor_Green : color -> Prop :=
| YNCg'  : yanextcolor_Green Orange.

Inductive yanextcolor_Orange : color -> Prop :=
| YNCo'  : yanextcolor_Orange Red.

Inductive yanextcolor_Red : color -> Prop :=
| YNCr'  : yanextcolor_Red Green.

Inductive yanextcolor_Purple : color -> Prop := .

(** Dispatching according to the pilot. *)
Definition yanextcolor_dispatch (c: color) : color -> Prop :=
  match c with
  | Indigo => yanextcolor_Indigo
  | Blue => yanextcolor_Blue
  | Yellow => yanextcolor_Yellow
  | Green => yanextcolor_Green
  | Orange => yanextcolor_Orange
  | Red => yanextcolor_Red
  | Purple => yanextcolor_Purple
  end.

(** Inversion lemma *)
Definition yanextcolor_inv {c1 c2}
  (ync : yanextcolor c1 c2) : yanextcolor_dispatch c1 c2 .
Proof.
  destruct ync as [ | | | | | | ]; econstructor; eassumption.
Defined.

(* --------------------------- *)

(** Using small inversions *)
Theorem yanextcolor3_smallinv :
  forall c1 c2 c3 c4,
    yanextcolor c1 c2 ->
    yanextcolor c2 c3 ->
    yanextcolor c3 c4 ->
    c4 = c1.
Proof.
  intros c1 c2 c3 c4 ync1 ync2 ync3.
  destruct ync1 as [ | | c d ync1' nc | | | | ].
  - Check (yanextcolor_inv ync2 : yanextcolor_Indigo c3).
    (** A proof of [yanextcolor_Indigo c3] in turn provides 2 cases:
        - [YYNCi1'], constraining [c4] to be [Purple]
        - [YYNCi2'], constraining [c4] to be some color [d],
          such that [yanextcolor Yellow c3] and [nextcolor c3 d]  *)
    destruct (yanextcolor_inv ync2) as [ | c3 d ync nc ].
    + destruct (yanextcolor_inv ync3).
    + (** Observe that [c3] will be replaced by [Yellow] everywhere *)
      destruct (yanextcolor_inv ync) as [ ].
      (** Zero cases for [nc] *)
      destruct (nextcolor_inv nc).
  - destruct (yanextcolor_inv ync2).
  - destruct (yanextcolor_inv ync1') as [ ].
    destruct (nextcolor_inv nc).
  - (** [Yellow] is followed by [Yellow], twice *)
    destruct (yanextcolor_inv ync2); destruct (yanextcolor_inv ync3); reflexivity.
  - destruct (yanextcolor_inv ync2); destruct (yanextcolor_inv ync3); reflexivity.
  - destruct (yanextcolor_inv ync2); destruct (yanextcolor_inv ync3); reflexivity.
  - destruct (yanextcolor_inv ync2); destruct (yanextcolor_inv ync3); reflexivity.
Qed.

(** A shorter script using combinations of tactics. *)
Reset yanextcolor3_smallinv.
Theorem yanextcolor3_smallinv :
  forall c1 c2 c3 c4,
    yanextcolor c1 c2 ->
    yanextcolor c2 c3 ->
    yanextcolor c3 c4 ->
    c4 = c1.
Proof.
  intros c1 c2 c3 c4 ync1 ync2 ync3.
  destruct ync1 as [ | | c d ync1' nc | | | | ];
    try (destruct (yanextcolor_inv ync2); destruct (yanextcolor_inv ync3); reflexivity).
  - destruct (yanextcolor_inv ync2) as [ | c3 d ync2' nc].
    + destruct (yanextcolor_inv ync3).
    + destruct (yanextcolor_inv ync2'); destruct (nextcolor_inv nc).
  - destruct (yanextcolor_inv ync1'); destruct (nextcolor_inv nc).
Qed.

Print yanextcolor3_smallinv. (** ~90 lines *)

(* ------------------------------------------------------------------ *)

(** *** Pros and cons *)
(**
 Tactic [inversion] is very convenient because it works without
 any preparatory work; but
 - it introduces hypotheses whose names are hard to control,
   which is bad for robustness of scripts; indeed,
   for predicates that are more complex than [nextcolor]
   (constructors with components), we get hypotheses named
   [H3], [H28]...and these names depend on the naming algorithm
   used by the version of Coq you use.
 - a number of those hypotheses are equalities to be immediatly
   removed with [subst].

 Conversely, small inversions presented here require an additional
 work.  However,
 - no "black magics", we go back to basic pattern matching;
 - its behavior is predictible and it is easy to know
   which hypotheses will be created and need a name;
 - as a bonus, proof terms are much smaller.
 - second bonus: small inversions succeed in some (complex) situations
   where standard inversion fails.

Automation?
  --> work in progress with Basile Gros and Pierre Corbineau
*)