(* begin hide *)
Require Import Arith.
Require Import Nat.
Require Import Coq.Program.Equality. (* dependent induction *)
Require Import Lia.
(* end hide *)

(** The _weak call-by-value lambda calulus_ is a simple variant of
    lambda calculus with simple abstractions and reduction rules. It
    enjoys strong uniform-confluence properties and is easy to reason
    with in machine proofs. *)

(** Like all lambda calculi, the language is built from variables,
    applications and abstractions. *)

Inductive term :=
| var (n: nat)
| app (s: term) (t: term)
| lambda (s: term).

(** The substitution rule describes how the bound variable in an
    abstraction is interpreted. The target variable increments up when
    passing through an abstraction. *)

Fixpoint subst (s: term) (n: nat) (t: term) :=
  match s with
  | var i => match (eqb n i) with true => t | false => var i end
  | app u v => app (subst u n t) (subst v n t)
  | lambda u => lambda (subst u (S n) t)
  end.

(** Terms are _closed_ if they are unaffected by substitutions.  A
    term is _bound_ by some [n] if it is unaffected by substitutions
    of variables of size [n] or greater. *)

Fixpoint bound (s: term) (n: nat) : Prop :=
  match s with
  | var i => i < n
  | app u v => (bound u n) /\ (bound v n)
  | lambda u => bound u (S n)
  end.

Definition closed (s: term) := bound s 0.

Definition variable (s: term) :=
  exists (n: nat), s = var n.

Definition application (s: term) :=
  exists (u v: term), s = app u v.

Definition abstraction (s: term) :=
  exists (u: term), s = lambda u.

(** A _combinator_ (called a _procedure_ by Forster and Smolka) is a
    closed abstraction. It is a function whose contents are not
    changed by higher level substitutions. *)

Definition combinator (s: term) := closed s /\ abstraction s.

(** * Boundedness Properties

    Below are some useful properties of boundedness. *)

Lemma bound_relaxes :
  forall (s: term) (m n: nat),
    m < n -> bound s m -> bound s n.
Proof.
  intros s.
  induction s as [k | u IHu v IHv | u IH].
  - simpl. intros m n. intros Hmn Hkm. 
    apply Nat.lt_trans with (p := n) (n := k) (m := m).
    apply Hkm. apply Hmn.
  - intros m n. simpl. intros Hmn HumAvm.
    destruct HumAvm as [Hum Hvm]. split.
    apply IHu with (m := m) (n := n). apply Hmn. apply Hum.
    apply IHv with (m := m) (n := n). apply Hmn. apply Hvm.
  - intros m n Hmn. simpl. apply IH with (m := S m) (n := S n).
    rewrite <- Nat.succ_lt_mono with (m := n) (n := m). apply Hmn.
Qed.
      
Lemma bound_subst :
  forall (s t: term) (i n: nat),
    bound s n -> bound t n -> bound (subst s i t) n.
Proof. intros s t. induction s as [j  | u IHu v IHv | u IHu].
       - simpl. intros i n Hij Hbound. destruct (i =? j).
         + apply Hbound. + simpl. apply Hij.
       - intros i n. simpl. intros HunAvn Htn.
         destruct HunAvn as [Hun Hvn]. split.
         apply IHu. apply Hun. apply Htn.
         apply IHv. apply Hvn. apply Htn.
       - intros i n. simpl. intros HuSn Htn.
         apply IHu with (i := S i) (n := S n).
         apply HuSn. apply bound_relaxes with (m := n) (n := S n).
         apply Nat.lt_succ_diag_r. apply Htn.
Qed.

Lemma subst_drops_bound :
  forall (s t: term) (n: nat),
    bound s (S n) -> bound t n -> bound (subst s n t) n.
Proof.
  intros s t.
  induction s as [k | u IHu v IHv | u IHu].
  - intros n Hsbound Htbound. simpl. simpl in Hsbound.
    destruct (n =? k) eqn:E.
    * apply Htbound.
    * rewrite Nat.lt_succ_r in Hsbound.
      rewrite Nat.eqb_neq in E.
      apply Nat.le_lteq in Hsbound.
      destruct Hsbound.
      { simpl. apply H. }
      { unfold "<>" in E. apply eq_sym in H.
        apply E in H. exfalso. apply H. }
  - intros n Hsbound Htbound. simpl. simpl in Hsbound.
    destruct Hsbound as [Hubound Hvbound]. split.
    + apply IHu. apply Hubound. apply Htbound.
    + apply IHv. apply Hvbound. apply Htbound.
  - intros n. intros Hsbound Htbound. simpl. simpl in Hsbound.
    apply IHu with (n := S n). apply Hsbound.
    apply bound_relaxes with (m := n) (n := S n).
    apply Nat.lt_succ_diag_r. apply Htbound.
Qed.

Lemma app_closed_iff :
  forall (s t: term), closed (app s t) <-> closed s /\ closed t.
Proof. intros s t. unfold closed. simpl. split.
       - intros H. apply H.
       - intros H. apply H.
Qed.

Lemma subst_preserves_closed :
  forall (u s t: term), s = lambda u -> closed s -> closed t ->
                        closed (subst u 0 t).
Proof.
  induction u.
  - intros s t Hsu Hsclosed Htclosed. simpl. destruct n.
    + apply Htclosed.
    + rewrite Hsu in Hsclosed. inversion Hsclosed.
      apply Nat.leb_le in H0. simpl in H0. discriminate H0.
  - intros s t Hsu Hsclosed Htclosed. simpl. apply app_closed_iff.
    rewrite Hsu in Hsclosed. inversion Hsclosed as [Hu1 Hu2]. split.
    + apply IHu1 with (s := lambda u1). reflexivity. apply Hu1. apply Htclosed.
    + apply IHu2 with (s := lambda u2). reflexivity. apply Hu2. apply Htclosed.
  - intros s t Hsu Hsclosed Htclosed. simpl. rewrite Hsu in Hsclosed.
    unfold closed in Hsclosed. simpl in Hsclosed.
    unfold closed. simpl.
    apply subst_drops_bound. apply Hsclosed.
    apply bound_relaxes with (m:=0) (n:=1).
    apply Nat.lt_succ_diag_r. apply Htclosed.
Qed.

Lemma bounds_block_subst :
  forall (s t: term) (k: nat), bound s k -> subst s k t  = s.
Proof.
  intros s. induction s.
  - intros t k. simpl. intros Hbound. destruct (k =? n) eqn:E.    
    + apply Nat.lt_neq in Hbound.
      apply Nat.eqb_eq in E. apply Nat.eq_sym in E.
      apply Hbound in E. exfalso. apply E.
    + reflexivity.
  - intros t k Hbound. inversion Hbound as [Hs1bound Hs2bound]. simpl.
    rewrite IHs1. rewrite IHs2. reflexivity. apply Hs2bound. apply Hs1bound.
  - intros t k Hbound. simpl in Hbound. simpl.
    rewrite IHs. reflexivity. apply Hbound.
Qed.


(** * Simple Combinators 

    Below are some examples of simple combinators written in the weak
    call-by-value language. 

    - [I]: identity
    - [T]: true branch (returns first of two inputs)
    - [F]: false branch (returns second of two inputs)
    - [omega]: self-applicator
    - [Omega]: infinite loop
 *)

Definition c_I := lambda (var 0).

Definition c_T := lambda (lambda (var 1)).

Definition c_F := lambda (lambda (var 0)).

Definition c_omega := lambda (app (var 0) (var 0)).

Definition c_Omega := lambda (app c_omega c_omega).

(** * Reflections

    It is helpful in several proofs to have reflections of equality,
    boundedness, closure and combinators as boolean methods. They are
    included below. *)

(** ** Equality  *)

Fixpoint term_eqb (x: term) (y: term) :=
  match x with
  | var i => match y with
             | var j => (eqb i j)
             | _ => false
             end
  | app ux vx => match y with
                 | app uy vy => andb (term_eqb ux uy) (term_eqb vx vy)
                 | _ => false
                 end
  | lambda ux => match y with
                 | lambda uy => term_eqb ux uy
                 | _ => false
                 end
  end.

Ltac absurd := simpl; intros H; inversion H.

Lemma term_eqb_compat :
  forall (x y: term), term_eqb x y = true <-> x = y.
Proof.
  induction x.
  - destruct y.
    + simpl. rewrite PeanoNat.Nat.eqb_eq.
      split.
      * intros H. rewrite H. reflexivity.
      *intros H. injection H as Heq. apply Heq.
    + simpl. split. absurd. absurd.
    + simpl. split. absurd. absurd.
  - destruct y.
    + simpl. split. absurd. absurd.
    + simpl. split.
      * intros Heq.
        apply eq_sym in Heq. apply Bool.andb_true_eq in Heq.
        destruct Heq as [H1 H2].
        apply eq_sym in H1. apply IHx1 in H1. rewrite H1.
        apply eq_sym in H2. apply IHx2 in H2. rewrite H2.
        reflexivity.
      * intros Heq. inversion Heq. rewrite <- H0. rewrite <- H1.
        apply andb_true_intro. split.
        { apply IHx1. reflexivity. } { apply IHx2. reflexivity. }
    + simpl. split. absurd. absurd.
  - destruct y.
    + simpl. split. absurd. absurd.
    + simpl. split. absurd. absurd.
    + simpl. rewrite IHx. split.
      * intros H. rewrite H. reflexivity.
      * intros H. injection H as Heq. apply Heq.
Qed.

(** ** Boundedness *)

Fixpoint is_bound (x: term) (n: nat) :=
  match x with
  | var i => ltb i n
  | app u v => andb (is_bound u n) (is_bound v n)
  | lambda u => is_bound u (S n)
  end.

Lemma is_bound_compat :
  forall (x: term) (n: nat), is_bound x n = true <-> bound x n.
Proof.
  induction x as [k | u Hu v Hv | u Hu]. 
  - intros n. simpl. apply PeanoNat.Nat.ltb_lt.
  - intros n. simpl. rewrite <- Hu. rewrite <- Hv.
    apply Bool.andb_true_iff.
  - intros n. simpl. rewrite <- Hu. apply iff_refl.
Qed.

(** ** Closure *)

Definition is_closed (x: term) := is_bound x 0.

Corollary is_closed_compat :
  forall (x: term), is_closed x = true <-> closed x.
Proof.
  unfold is_closed. unfold closed. intros x.
  apply is_bound_compat.
Qed.

(** ** Abstraction *)

Definition is_abstraction (x: term) : bool :=
  match x with
  | lambda u => true
  | _ => false
  end.

Lemma is_abstraction_compat :
  forall (x: term), is_abstraction x = true <-> abstraction x.
Proof.
  destruct x.
  - simpl. split.
    + intros H. inversion H.
    + intros H. inversion H as [u Hu]. inversion Hu.
  - simpl. split.
    + intros H. inversion H.
    + intros H. inversion H as [u Hu]. inversion Hu.
  - simpl. split.
    + intros _. exists x. reflexivity.
    + reflexivity.
Qed.

(** ** Combinator *)

Definition is_combinator (x: term) :=
  andb (is_abstraction x) (is_closed x).

Lemma is_combinator_compat :
  forall (x: term), is_combinator x = true <-> combinator x.
Proof.
  intros x. unfold is_combinator. unfold combinator.
  rewrite <- is_closed_compat. rewrite <- is_abstraction_compat.
  rewrite Bool.andb_comm. apply Bool.andb_true_iff.
Qed.

(** ** Substitution *)

Definition predicate (x: term) :=
  match x with
  | lambda u => u
  | _ => x
  end.

Definition combine (f x: term) := subst (predicate f) 0 x.