(**
Initiation to inductively defined relations.
*)

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

(** * Predicates with 1 argument on an enumerated type  *)

(** Let us start with a very simple predicate that indicates how
    to select some values in an enumerated type. *)


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

(** Reminder: defining a type sharing constructors with another already
    defined type is NOT allowed. *)
Fail Inductive tlcolor : Set :=
| Green  : tlcolor
| Orange : tlcolor
| Red    : tlcolor
.

(** Why is it forbidden? *)

(** But we can define a predicate on [color] that can be proved
    for [Green] [Orange] and [Red] (and only for them). *)

Inductive is_tlcolor : color -> Prop :=
| Tgre : is_tlcolor Green
| Tora : is_tlcolor Orange
| Tred : is_tlcolor Red
.

(** Forget the following alternatives!
    No point to explain one simple inductive type
    using two complicated parameterized inductive types,
    and to manage additional complications due to the binary
    nature of \/.
*)
Definition is_tlcolor_alt  := fun c => (c = Green \/  c = Orange) \/ c = Red.
Definition is_tlcolor_alt' := fun c =>  c = Green \/ (c = Orange  \/ c = Red).

(** For example we can show that [Green] satisfies this predicate. *)
Example example_tl_Green : is_tlcolor Green.
Proof.
  apply Tgre.
Qed.

(** Some traffic lights use only the two colors Green and Red. *)

Inductive tl2color : color -> Prop :=
| T2gre : tl2color Green
| T2red : tl2color Red
.

(** Let us show that the latter predicate entail the former. *)

Lemma tl2color_is_tlcolor : forall c, tl2color c -> is_tlcolor c.
Proof.
  intro c.
  (** We first try to reson by case on [c].*)
  destruct c.
  (** Many useless cases (requiring, moreeover, a special technique).
      Let us then try a better strategy. *)
  Undo 1.
  (** Introduction of the hypothesis on [c]. *)
  intro t2c.
  (** It is enough to reason by cases on the 2 possible ways
      of constructing [t2c] *)
  refine (match t2c with T2gre => _ | T2red => _ end).
  clear.
  (** We get the same effect by using [destruct] on the HYPOTHESIS [t2c] *)
  Undo 2.
  destruct t2c as [ (*T2gre*) | (*F2rou*) ].
  - apply Tgre.
  - refine Tred.
Qed.

(** Training exercise *)

(** On the model of predicate [is_tlcolor], define un another predicate named
    [fivecol], that selects colors Blue, Orange, Indigo, Green and Red. *)

(* [Inductive fivecol] TO BE COMPLETED *)

Inductive fivecol : color -> Prop :=.

(** Then prove: *)

Lemma is_tlcolor_fivecol : forall c, is_tlcolor c -> fivecol c.
Proof.
  (** COMPLETΕ HERE *)
Admitted.

(** ** Relations with 2 arguments on an enumerated type *)

(** Inductive relations allow us to represent partial fonctions, i.e.,
    functions that are not defined everywhere. Here is an example where
    [nextcolor] is defined for Green, Orange et Red, but not for the
    other colors given in [color]. *)

Inductive nextcolor : color -> color -> Prop :=
| CSv : nextcolor Green Orange
| CSo : nextcolor Orange Red
| CSr : nextcolor Red Green
.

(** Exercise (same technique as before) *)

Lemma nextcolor_is_tlcolor : forall c1 c2, nextcolor c1 c2 -> is_tlcolor c1.
Proof.
  (** COMPLETΕ HERE *)
Admitted.

(** ** Predicate [even] on [nat] *)

(** Just as inductive data types can be recursive,
    for example [nat] or [aexp], inductive predicates can be
    recursive. This is the case of [even], defined as follows. *)

Inductive even : nat -> Prop :=
| E0 : even 0
| E2 : forall n, even n -> even (S (S n))
.

(** Exercise : show that 6 is even. *)

Example ev10 : even 10.
Proof.
  refine (E2 8 _).
  apply (E2 6).
  apply E2.
  (** COMPLETE HERE *)
Admitted.

(** [even] has the same structure as a list of numbers, but it enforces
    these numbers to be 0, 2, 4... from right to left *)
Print ev10.

(*
       ------- E0
       even 0
       ------- E2 0
       even 2
       ------- E2 2
       even 4
       ------- E2 4
       even 6
       ------- E2 6
       even 8
       ------- E2 8
       even 10

   similar to Cons 8 (Cons 6 (Cons 4 (Cons 2 Nil)))


*)

(**

General shape of a proof tree, made of proof rules;
each label is the name of the proof rule used in order
to justify the conclusion form the immediate premises
above the bar. For proof-trees correponding to inductive
realtions, the labels are simple their constructors
(applied to suitable arguments, e.g., [E2 4)).


                        :
         :           premise4
      -------- l1    -------- l2       :
      premise1       premise2       premise3
     ---------------------------------------- label
                   conclusion


A well-known rule:

         A -> B     A
         ------------ modus ponens
              B

 *)

(** Questions :
    - what is the type and the meaning of [E2 4] ?
    - what is the type and the meaning of [E2 5] ?
 *)


(** Numbers that can be reached by adding 2s or 7s starting from 0. *)
Inductive p2p7 : nat -> Prop :=
| PP0 : p2p7 0
| PP2 : forall n, p2p7 n -> p2p7 (2 + n)
| PP7 : forall n, p2p7 n -> p2p7 (7 + n)
.

(** Exercise : prove in 3 different ways that 11 is reachable using [p2p7]. *)
Example p2p7_11_method1 : p2p7 11.
Proof.
  (** COMPLETE HERE *)
Admitted.

Example p2p7_11_method2 : p2p7 11.
Proof.
  (** COMPLETE HERE *)
Admitted.

Example p2p7_11_method3 : p2p7 11.
Proof.
  (** COMPLETE HERE *)
Admitted.

Print p2p7_11_method2.

(** Show that all even numbers satisfy [p2p7]. *)

Theorem even_p2p7 : forall n, even n -> p2p7 n.
Proof.
  intros n evn.
  (** As there are infinitely many even integers, a proof by case
      is not powerful enough. We proceed by structural induction on the
      possible ways to prove [even n], in other words, the possible forms
      of proof trees for [evn] made of constructors.
      We have 2 cases, the case where [evn] is [E0], and the case where
      [evn] is of the form [E2 n' evn'], with [evn' : even n'];
      in the latter case, we get an induction hypothesis on [evn'],
      ensuring that [n'] satisfies [p2p7].
  *)
  induction evn as [ (*E0*) | (*E2*) n' evn' IH_evn'].
  - apply PP0.
  - (** Optional: put in a form clearly adapted to [p2p7] *)
    change (p2p7 (2 + n')).
    (** Using the relevant constructor of [p2p7] *)
    apply PP2.
    (** Using the induction hypothesis *)
    apply IH_evn'.
Qed.

(** It is instructive to prove the same theorem by a recursive function. *)

Fixpoint fct_even_p2p7 n (evn : even n) : p2p7 n :=
  match evn with
  | E0 => PP0
  | E2 n' evn' => PP2 n' (fct_even_p2p7 n' evn')
  end.

(** From a proof tree of [even 4] given in input, we can get a proof tree
    of [p2p7 4] *)
Compute fct_even_p2p7 4 (E2 2 (E2 0 E0)).

(** Reminder: functions defined using a [Qed] cannot be computed. *)
Compute even_p2p7 4 (E2 2 (E2 0 E0)).

(** Exercise: the sum of two even numbers is even *)
Lemma even_plus : forall n m, even n -> even m -> even (n + m).
Proof.
  intros n m evn evm.
  (** Complete by structural induction on [evn] *)
Admitted.

(** Optional exercise:
    give a proof in the form of a function. *)

Fixpoint fct_even_plus n m (evn : even n) (evm : even m) : even (n + m).
  (** COMPLETE HERE *)
Admitted.

(* Exercise: multiples of 4 are even *)
Inductive mul4 : nat -> Prop :=
| M4_0 : mul4 0
| M4_4 : forall n, mul4 n -> mul4 (S (S (S (S n))))
.

Lemma mul4_even : forall n, mul4 n -> even n.
Proof.
  intros n m4n.
  (** COMPLETE using structural induction on [m4n] *)
Admitted.

(* ============================================================================== *)
(* Second part : material to be presented later *)

(** ** Equality *)

(** Equality is a nothing but a special inductive relation *)

Print is_tlcolor.

(** Consider a similar predicate with exactly 1 case *)

Inductive is_Green : color -> Prop :=
| IG_intro : is_Green Green.

Lemma Green_is_tlcolor : forall c, is_Green c -> is_tlcolor c.
Proof.
  intros c ig. destruct ig (** c is replaced by Green -- nothing new! *).
  Undo. (** Effect only on the conclusion *)
  refine (match ig with IG_intro => _ end).
  Undo. (** Shorter tactic: [case] *)
  case ig.
  constructor.
Qed.

(** Generalization to an abstract color *)
Section sec_is_this_color.
  Variable c : color.

  Inductive is_this_color : color -> Prop :=
  | itc_intro : is_this_color c.

  Lemma only_one : forall x y, is_this_color x -> is_this_color y -> x = y.
  Proof.
    intros x y itc_x itc_y.
    refine (match itc_x with itc_intro => _ end).
    case itc_y.
    reflexivity.
  Qed.
  
End sec_is_this_color.

Print is_this_color.

(** Even more abstract *)
Section sec_is_this_thing.
  Variable A : Type.

  Inductive eqA : A -> A -> Prop :=
    | eqA_refl : forall x, eqA x x.
  
  Variable x : A.

  Inductive is_this_thing : A -> Prop :=
  | itt_intro : is_this_thing x.

  Lemma only_one_thing : forall a b, is_this_thing a -> is_this_thing b -> a = b.
  Proof.
    intros a b itc_a itc_b.
    case itc_a. case itc_b.
    reflexivity.
  Qed.
  
End sec_is_this_thing.

Print is_this_thing.
Print eq.

Check eq_ind.
Check is_this_thing_ind.
Check eqA_ind.
Print eq_ind.
Check nat_ind.
Print nat_ind.
Check eq_sym.
Print eq_sym.
Check eq_ind_r.

(** 
    - basically, [rewrite <-] is just a [case] 
    - [rewrite] is derived from [rewrite <-]
*)

(* ============================================================================== *)
(* Third part : material to be presented after extraction *)

(** Extraction of a correct-by-construction recursive OCaml program *)

(* ------------------------ *)
(** Small inversion of even *)
Inductive even0 : Prop := E0' : even0.
Inductive even1 : Prop := .
Inductive evenSS (n : nat) : Prop := E2' : even n -> evenSS n.
Definition even_dispatch (n : nat) : Prop :=
  match n with
  | 0       => even0
  | 1       => even1
  | S (S n) => evenSS n
  end.
Lemma even_inv {n} (ev : even n) : even_dispatch n.
Proof. destruct ev; constructor; assumption. Qed.
(* ------------------------ *)

Fixpoint half (n : nat) : even n -> {y | y + y = n}.
Proof.
  refine(
  match n with
  | 0       => fun ev => _
  | 1       => fun ev => _
  | S (S n) => fun ev => let (y, e) := half n _ in _
  end).
  - exists 0. reflexivity.
  - destruct (even_inv ev).
  - destruct (even_inv ev) as [evn]. exact evn.
  - exists (S y). cbn. apply f_equal. rewrite <- e.
    rewrite <- plus_n_Sm. reflexivity.
Defined.

Print half.

Compute half 10 ev10.
Eval lazy in half 10 ev10.

Definition resu_half n ev := let (y, _) := half n ev in y.

Compute resu_half 10 ev10.
Eval lazy in resu_half 10 ev10.


Require Import Extraction.
Recursive Extraction half.

(* ============================================================================== *)
(* Forth part : material to be presented before Braga *)

Print Acc.
Print well_founded.

Print Nat.add.

Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
  Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x.

Definition well_founded {A : Type} (R : A -> A -> Prop) :=
  forall a : A, Acc R a.

(** Standard way of defining functions *)

Lemma all_acc : well_founded sometype R.

Fixpoint myfct (x : sometype) (acc : Acc R x) {struct acc} := ...
     myfct y (Acc_inv c acc ryx) ...

Check Acc_inv : forall (A : Type) (R : A -> A -> Prop) (x : A),
       Acc R x -> forall y : A, R y x -> Acc R y.
  

Print Wf.

(** See Equations, by M. Sozeau, "Functional Induction"
  Well-founded recursion done right, X. Leroy
 *)