From Coq Require Import Relations List.
Import ListNotations.

Inductive tm : Type :=
  | tTrue  : tm
  | tFalse : tm
  | tIf (b t t' : tm) : tm.

Inductive value : tm -> Prop :=
  | v_true : value tTrue
  | v_false : value tFalse.


Inductive one_red : tm -> tm -> Prop :=
| ored_true t u : one_red (tIf tTrue t u) t
| ored_false t u : one_red (tIf tFalse t u) u
| ored_if b b' t u :
    one_red b b' -> one_red (tIf b t u) (tIf b' t u).


Inductive clos_refl_trans {A : Type} (R : A -> A -> Prop) :
A -> A -> Prop :=

| rt_refl (x : A) : clos_refl_trans R x x
| rt_step (x y : A) : R x y -> clos_refl_trans R x y
| rt_trans (x y z : A) :
    clos_refl_trans R x y ->
    clos_refl_trans R y z ->
    clos_refl_trans R x z.

Definition red := clos_refl_trans one_red.


Lemma val_nf t :
  value t -> ~ (exists t', one_red t t').
Proof.
Admitted.

(** Custom induction *)

Lemma val_red t t' :
  value t -> red t t' -> t = t'.
Abort.

Lemma clos_refl_trans_ind_right (A : Type)
  (R : A -> A -> Prop) (P : A -> A -> Prop) :
  (forall z, P z z) ->
  (forall x y z : A,
    R x y -> clos_refl_trans R y z -> P y z -> P x z) ->
  forall (x z : A), clos_refl_trans R x z -> P x z.
Proof.
  intros Hrefl Hstep x z H.
  set (P' := fun x => P x z).
  assert (Hrefl' : P' z) by (unfold P' ; auto).
  assert (Hstep' : forall x y, R x y -> clos_refl_trans R y z -> P' y -> P' x)
    by (unfold P' ; eauto).
  change (P' x).
  clearbody P'.
  clear Hrefl Hstep.
  induction H as [ | | x y z Hx IHx Hy IHy].
  - apply Hrefl'. 
  - eapply Hstep' ; try eauto.
    constructor.
  - assert (P' y) by (apply IHy ; auto).
    apply IHx ; auto.
    intros.
    eapply Hstep' ; eauto.
    eapply rt_trans ; eauto.
Qed.

Lemma val_red t t' :
  value t -> red t t' -> t = t'.
Proof.
  intros Hv Hred.
  unfold red in Hred.
  induction Hred using clos_refl_trans_ind_right.
  - reflexivity.
  - exfalso.
    eapply val_nf.
    1: eassumption.
    eexists.
    eassumption.
Qed.

(** ** Predicates as functions *)

Definition is_value (t : tm) : Prop :=
  match t with
  | tTrue => True
  | tFalse => True
  | tIf _ _ _ => False
  end.

Compute (I : is_value tTrue).

(** An alternative way, using booleans *)
Require Import Bool ssrbool.

Fixpoint nat_eqb (m n : nat) : bool :=
  match m, n with
  | 0, 0 => true
  | S _, 0 | 0, S _ => false
  | S m', S n' => nat_eqb m' n'
  end.

Lemma nat_eqb_refl (m : nat) : nat_eqb m m = true.
Proof.
  induction m.
  - simpl.
    reflexivity.
  - simpl. assumption.
Qed.

Lemma nat_eqb_sound (m n : nat) : nat_eqb m n = true -> m = n.
Proof.
  intros He.
  induction m in n, He |- *.
  - destruct n ; simpl ; easy.
  - destruct n ; simpl in *.
    1: easy.
    erewrite IHm ; eauto.
Qed.

Print reflect.

Lemma eqb_correct (m n : nat) : reflect (m = n) (nat_eqb m n).
Proof.
  apply iff_reflect ; split.
  - intros. subst.
    apply nat_eqb_refl.
  - apply nat_eqb_sound.
Qed.

(** Using reflect *)

Lemma match_test (m n : nat) :
  (match (nat_eqb m n) with | true => 0 | false => 1 end = 1) ->
  m <> n.
Proof.
  destruct (eqb_correct m n).
  - easy.
  - easy.
Qed.

(** There are many variations!
  It's powerful to be able to go back and forth. *)

(** Remember the difference between definitional,
  propositional and boolean equality. *)