1 files changed, 321 insertions, 0 deletions
diff --git a/theories/L.v b/theories/L.v
new file mode 100644
index 0000000..e9b8417
--- /dev/null
+++ b/theories/L.v
@@ -0,0 +1,321 @@
+(* 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.