From Coq Require Import Relations List.
Import ListNotations.

(** Inductive types *)

Print nat.

Print list.

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

(** Indexed inductive types/predicates *)

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

  
About value.
Check (value tTrue).
Check (v_true).
Check (value (tIf tTrue tTrue tTrue)).
Check value_ind.

(* Of course, we can have recursive predicates too *)

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).

About one_red_ind.

(* With parameters *)

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.
    
About clos_refl_trans_ind.

Definition red := clos_refl_trans one_red.

Lemma red_if b b' t u :
  red b b' -> red (tIf b t u) (tIf b' t u).
Proof.
  intros H.
  unfold red in H.
  induction H.
  - constructor.
  - apply rt_step.
    constructor.
    assumption.
  - apply rt_trans with (tIf y t u).
    all: assumption.
Qed.

Lemma val_nf t :
  value t -> ~ (exists t', one_red t t').
Proof.
  intros Hv.
  destruct Hv.
  - intros Ht.
    destruct Ht as [t' Ht].
    inversion Ht.
  - intros Ht.
    destruct Ht as [t' Ht].
    inversion Ht.
Qed.

Lemma val_red t t' :
  value t -> red t t' -> t = t'.
Proof.
  intros Hv Hred.
  induction Hred as [x | x y HR | x y z Hx IHx Hy IHy].
  - reflexivity.
  - exfalso.
    apply (val_nf x).
    1: assumption.
    exists y.
    assumption.
  - specialize (IHx Hv).
    subst.
    specialize (IHy Hv).
    subst.
    reflexivity.
Qed.

(** Custom induction *)

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.