Simple build and README.

1 files changed, 553 insertions, 0 deletions

diff --git a/theories/Evaluation.v b/theories/Evaluation.v
new file mode 100644
index 0000000..48b8fdc
--- /dev/null
+++ b/theories/Evaluation.v
@@ -0,0 +1,553 @@
+(* begin hide *)
+Require Import Arith.
+Require Import Nat.
+Require Import Coq.Program.Equality. (* dependent induction *)
+Require Import Lia.
+Require Import Bool.
+(* end hide *)
+Require Import L.
+
+(** Evaluation captures the idea of computation in lambda calculus.
+    When simplifying terms by hand, we look for applications of
+    abstractions to perform reductions. It's not obvious a-priori what
+    order these applications should be performed in, or whether the
+    results are always the same. *)
+
+(** The _evaluation_ relation is defined in terms of substitution. It
+    makes no obvious choices about the order of substitutions. *)
+
+Inductive evaluates_to: term -> term -> Prop :=
+| refl s t u: (s = lambda u) -> (t = lambda u) -> evaluates_to s t
+| eval s t u v w:
+  evaluates_to s (lambda u) -> evaluates_to t v ->
+  evaluates_to (subst u 0 v) w -> evaluates_to (app s t) w.
+
+Definition evaluates (s: term) : Prop :=
+  exists t, evaluates_to s t.
+
+(** * Evaluation Properties 
+
+    Evaluation is slightly tricky to analyze because it has
+    flexibility in the terms which are actually substituted. Proving
+    statements about evaluation usually involves analyzing the actual
+    reductions which can occur, and the details of this are deferred
+    until later.  Some simple statements about evaluation, particularly
+    in relation to closed terms and abstractions are easy to show from
+    the inductive definition. *)
+
+Lemma only_can_evaluate_to_abstr :
+  forall (s t: term), evaluates_to s t -> abstraction t.
+Proof.
+  intros s t Heval.
+  induction Heval.
+  - unfold abstraction. exists u. apply H0.
+  - apply IHHeval3.
+Qed.
+
+Lemma evaluation_preserves_closure :
+  forall (s t: term), closed s -> evaluates_to s t -> closed t.
+Proof.
+  intros s t Hclosed Heval. induction Heval.
+  + rewrite H0. rewrite <- H. apply Hclosed.
+  + inversion Hclosed as [Hsclosed Htclosed].
+    apply IHHeval3. apply subst_preserves_closed with (s := lambda u).
+    reflexivity.
+    apply IHHeval1. apply Hsclosed.
+    apply IHHeval2. apply Htclosed.
+Qed.
+
+Lemma if_app_evaluates_then_both_evaluate :
+  forall (s t: term), evaluates (app s t) -> evaluates s /\ evaluates t.
+Proof.
+  intros s t.
+  intros Heval. inversion Heval as [s' Heval']. inversion Heval'.
+  - discriminate H.
+  - unfold evaluates. split.
+    + exists (lambda u). apply H1.
+    + exists v. apply H2.
+Qed.
+
+Lemma evaluate_not_closed_wrt_app :
+  exists (s t: term), evaluates s /\ evaluates t /\ ~ (evaluates (app s t)).
+Proof.
+  exists (lambda (var 1)). exists (lambda (var 1)).
+  assert (evaluates (lambda (var 1))) as Hlv1eval.
+  { unfold evaluates. exists (lambda (var 1)).
+    apply refl with (u := var 1). reflexivity. reflexivity. }
+  split. apply Hlv1eval. split. apply Hlv1eval.
+  unfold "~". intros Happeval. inversion Happeval.
+  inversion H.
+  - discriminate H0.
+  - inversion H2. 
+    + injection H6 as Hu0def.
+      injection H7 as Hudef.
+      rewrite <- Hu0def in Hudef.
+      rewrite Hudef in H5. simpl in H5.
+      inversion H5. discriminate H6.
+Qed.
+
+Lemma evaluation_is_transitive :
+  forall (a b c: term),
+    evaluates_to a b -> evaluates_to b c -> evaluates_to a c.
+Proof.
+  intros a b c Hab Hbc. dependent induction Hbc.
+  - rewrite H0. rewrite H in Hab. apply Hab.
+  - apply only_can_evaluate_to_abstr in Hab.
+    inversion Hab as [x Hx]. discriminate Hx.
+Qed.
+
+(** * Reduction
+    
+    To study the evaluation of lambda terms we need to understand the
+    behaviours of chains of valid substitutions. This is done with the
+    concept of a _reduction_. It turns out that an evaluation exists
+    exactly when there is a reduction to an abstraction. *)
+
+(** Larger reductions are built from _one-step reductions_ which are
+    simply substitutions.
+
+    A term _[n]-step reduces_ to another if a sequence of [n] one-step
+    reductions translate the initial term into the final one.
+
+    One term _reduces_ to another if the two terms are literally equal
+    or can be built from one-step reductions. *)
+
+Inductive one_step_reduces_to : term -> term -> Prop :=
+| one_step_sub s t : one_step_reduces_to (app (lambda s) (lambda t)) (subst s 0 (lambda t))
+| one_step_appl s s' t : one_step_reduces_to s s' -> one_step_reduces_to (app s t) (app s' t)
+| one_step_appr s t t' : one_step_reduces_to t t' -> one_step_reduces_to (app s t) (app s t').
+
+Inductive n_step_reduces_to : nat -> term -> term -> Prop :=
+| n_step_refl s : n_step_reduces_to 0 s s
+| n_step_incr n s u t : one_step_reduces_to s u -> n_step_reduces_to n u t ->
+                        n_step_reduces_to (S n) s t.
+
+Inductive reduces_to : term -> term -> Prop :=
+| reduces_to_refl s : reduces_to s s
+| reduces_to_incr s u t : one_step_reduces_to s u -> reduces_to u t ->
+                          reduces_to s t.
+
+(** There are a variety of properties which we can prove about
+    reductions alone. *)
+
+(** ** [n]-Step Reduction Properties *)
+
+Lemma n_step_transitivity :
+  forall (n m : nat) (x y z: term),
+    n_step_reduces_to n x y -> n_step_reduces_to m y z ->
+    n_step_reduces_to (n + m) x z.
+Proof.
+  intros n. induction n. 
+  - intros m x y z Hxy Hyz. simpl. inversion Hxy. apply Hyz.
+  - intros m x y z Hxy Hyz. inversion Hxy.
+    rewrite plus_Sn_m. apply n_step_incr with (u:=u).
+    apply H0. apply IHn with (y:=y). apply H1. apply Hyz.
+Qed.
+
+Lemma n_step_additive :
+  forall (n m: nat) (s u t: term),
+    n_step_reduces_to n s u -> n_step_reduces_to m u t ->
+    n_step_reduces_to (n + m) s t.
+Proof.
+  intros n m. induction n.
+  - intros s u t Hnsu Hmut.
+    Search "+". rewrite Nat.add_0_l. destruct m.
+    + inversion Hnsu. apply Hmut.
+    + inversion Hnsu. apply Hmut.
+  - intros s u t Hsnsu Hmut.
+    Search "+". rewrite plus_Sn_m.
+    inversion Hsnsu. apply n_step_incr with (u := u0).
+    apply H0. apply IHn with (u := u). apply H1. apply Hmut.
+Qed.
+
+(** ** Reduction Properties *)
+
+Lemma reduction_is_transitive :
+  forall (r s t : term), reduces_to r s -> reduces_to s t -> reduces_to r t.
+Proof.
+  intros r s t Hrs Hst.
+  dependent induction Hrs.
+  - apply Hst.
+  - apply reduces_to_incr with (s:=s) (u:=u) (t:=t).
+    apply H. apply IHHrs. apply Hst.
+Qed.
+
+Lemma reduction_left_applicative :
+  forall (s t t': term), reduces_to t t' -> reduces_to (app s t) (app s t').
+Proof.
+  intros s t t' Htt'. induction Htt'.
+  - apply reduces_to_refl.
+  - apply reduces_to_incr with (u := app s u).
+    apply one_step_appr. apply H. apply IHHtt'.
+Qed.
+
+Lemma reduction_right_applicative :
+  forall (s s' t: term), reduces_to s s' -> reduces_to (app s t) (app s' t).
+Proof.
+  intros s s' t Hss'. induction Hss'.
+  - apply reduces_to_refl.
+  - apply reduces_to_incr with (u := app u t).
+    apply one_step_appl. apply H. apply IHHss'.
+Qed.
+
+Lemma reduction_applicative :
+  forall (s s' t t': term), reduces_to s s' -> reduces_to t t' ->
+                            reduces_to (app s t) (app s' t').
+Proof.
+  intros s s' t t' Hss' Htt'.
+  apply reduction_is_transitive with (s := app s t').
+  apply reduction_left_applicative. apply Htt'.
+  apply reduction_right_applicative. apply Hss'.
+Qed.
+
+Lemma reduction_is_realized :
+  forall (s t: term), reduces_to s t <->
+                      exists (n : nat), n_step_reduces_to n s t.
+Proof.
+  intros s t. split.
+  - intros Hst. induction Hst.
+    + exists 0. apply n_step_refl.
+    + inversion IHHst as [k Hut]. exists (S k).
+      apply n_step_incr with (n := k) (s:=s) (u := u) (t := t).
+      apply H. apply Hut.
+  - assert (forall (n: nat), forall (x y: term),
+               n_step_reduces_to n x y -> reduces_to x y) as Hsteps.
+    { intros n. induction n.
+      - intros x y Hnxy. inversion Hnxy. apply reduces_to_refl.
+      - intros x y Hsnxy. inversion Hsnxy.
+        apply reduces_to_incr with (u := u).
+        apply H0. apply IHn in H1. apply H1. }
+    intros Hred. inversion Hred. apply Hsteps in H. apply H.
+Qed.
+
+(** ** Properties of Possible Terms in Reduction
+
+    Often it is useful to reason about the possible terms that can be
+    the inputs and outputs of reductions. Below are some useful lemmas
+    in that vein. *)
+
+Lemma must_one_step_reduce_from_application :
+  forall (s t: term), one_step_reduces_to s t ->
+                      exists (s1 s2: term), s = app s1 s2.
+Proof.
+  intros s t Hst. inversion Hst.
+  - exists (lambda s0). exists (lambda t0). reflexivity.
+  - exists s0. exists t0. reflexivity.
+  - exists s0. exists t0. reflexivity.
+Qed.
+
+Lemma var_n_step_reduces_to_var :
+  forall (n k: nat) (s: term), n_step_reduces_to n (var k) s ->
+                               s = var k /\ n = 0.
+Proof.
+  intros n k s Hred. inversion Hred.
+  - split. reflexivity. reflexivity.
+  - apply must_one_step_reduce_from_application in H.
+    inversion H. inversion H4. discriminate H5.
+Qed.
+
+Lemma var_reduces_to_var :
+  forall (n: nat) (t: term), reduces_to (var n) t -> t = var n.
+Proof.
+  intros n t Hred.
+  apply reduction_is_realized in Hred. inversion Hred as [k Hkred].
+  specialize var_n_step_reduces_to_var with (n := k) (k := n) (s:=t) as Hvar.
+  destruct Hvar. apply Hkred. apply H.
+Qed.
+
+Lemma abs_reduces_to_abs :
+  forall (u t: term), reduces_to (lambda u) t -> t = lambda u.
+Proof.
+  intros u t Hred. apply reduction_is_realized in Hred.
+  inversion Hred as [k Hk]. inversion Hk. reflexivity. inversion H.
+Qed.
+
+(** * Relationships between Evaluation and Reduction 
+
+    Below are a few useful relationships between evaluation and
+    reduction. There are also some rules for extending evaluations
+    with reductions. Using these rules we can show that evaluation is
+    the same as a reduction to an abstraction. *)
+
+Lemma one_step_reduction_extends_evaluation :
+  forall (a b c: term),
+    one_step_reduces_to a b -> evaluates_to b c -> evaluates_to a c.
+Proof.
+  (* We want to use the one step reduction to extend the evaluation's
+     reach. We induct upon the one step reduction.
+
+     1. [base, substitution]. Here we have as evidence that
+        - a = app (lambda sa) (lambda ta)
+        - b = subst sa 0 (lambda ta)
+        and we want to show that
+        evaluates_to b c -> evaluates_to a c.
+        It's trivial to show that (evaluates_to a b), and the case
+        follows by the transitivity of evaluates_to.
+
+     2. [inductive, left-application]. Here we have as evidence:
+        - one_step_reduces_to ar ar'
+       - one_step_reduces_to (app al ar) (app al ar')
+        and the inductive hypothesis:
+        - forall t, one_step_reduces_to ar ar' ->
+                 evaluates_to ar' t -> evaluates_to ar t.
+        We want to show that
+        forall t, evaluates_to (app al ar') t ->
+               evaluates_to (app al ar) t.
+        In the evidence for evaluates_to (app al ar') t, we know that
+        there is some v used as input to the substitution for which
+        evaluates_to ar' v. By the inductive hypothesis, we then have
+        that evaluates_to ar v. That is enough to build the evidence
+        for evaluates_to (app al ar) t.
+
+     3. [inductive, right-application]. This is the same as the second
+     case, except instead of pulling-back the evidence for the
+     (evaluates_to t v) term, we pull back the evidence for the
+     (evaluates_to s (lambda u)) using the inductive hypothesis. *)
+  assert (forall (a b: term), one_step_reduces_to a b ->
+    forall (c: term), evaluates_to b c -> evaluates_to a c) as Htgt.
+  { intros a b Honestep. induction Honestep.
+    - intros c. intros Hbc. apply eval with (u := s) (v := lambda t) (w := c).
+      apply refl with (u := s). reflexivity. reflexivity.
+      apply refl with (u := t). reflexivity. reflexivity.
+      apply Hbc.
+    - intros c Hbc. inversion Hbc.
+      + discriminate H.
+      + apply IHHonestep in H1. apply eval with (u := u) (v := v).
+        apply H1. apply H2. apply H4.
+    - intros c Hbc. inversion Hbc.
+      + discriminate H.
+      + apply IHHonestep in H2. apply eval with (u := u) (v := v).
+        apply H1. apply H2. apply H4. }
+  intros a b c Hab. apply Htgt. apply Hab.
+Qed.
+
+Lemma reduction_extends_evaluation :
+  forall (a b c: term),
+    reduces_to a b -> evaluates_to b c -> evaluates_to a c.
+Proof.
+  intros a b c Hab. induction Hab.
+  + intros Hbc. apply Hbc.
+  + induction Hab.
+    - intros Hs0c. apply one_step_reduction_extends_evaluation with (b:=s0).
+      apply H. apply Hs0c.
+    - intros Htc. apply IHHab in Htc.
+      apply one_step_reduction_extends_evaluation with (b:=s0).
+      apply H. apply Htc.
+Qed.
+
+Proposition evaluation_iff_reduction_to_abstraction :
+  forall (s t: term), evaluates_to s t <->
+                      reduces_to s t /\ abstraction t.
+Proof.
+  split.
+  - intros Heval. split.
+    + induction Heval.
+      * rewrite H. rewrite H0. apply reduces_to_refl.
+      * assert (abstraction v) as Hvabstr.
+        { apply only_can_evaluate_to_abstr in Heval2. apply Heval2. }
+        assert (one_step_reduces_to (app (lambda u) v) (subst u 0 v)) as Huvsubst.
+        { inversion Hvabstr. specialize one_step_sub with (s := u) (t := x) as Hsub.
+          rewrite <- H in Hsub. apply Hsub. }
+        assert (reduces_to (app s t) (subst u 0 v)) as Hstred.
+        { apply reduction_is_transitive with (s := app (lambda u) v).
+          apply reduction_applicative. apply IHHeval1. apply IHHeval2.
+          apply reduces_to_incr with (u := subst u 0 v). apply Huvsubst.
+          apply reduces_to_refl. }
+        apply reduction_is_transitive with (s := subst u 0 v).
+        apply Hstred. apply IHHeval3.
+    + apply only_can_evaluate_to_abstr in Heval. apply Heval.
+  - intros [Hred Habstr].
+    apply reduction_extends_evaluation with (a:=s) (b:=t) (c:=t).
+    apply Hred. inversion Habstr as [u Hu]. apply refl with (u:=u).
+    apply Hu. apply Hu.
+Qed.
+
+(* lia: "linear integer arithmetic" (rocq manual 2025)
+   lia is used for deciding simple inequalities in integer arithmetic.
+
+   ltac: "L_{tac}" or "Tactic Language" (rocq manual 2025)
+   ltac is used for building tactics to streamline proofs.
+   it is deprecated for ltac2, as ltac grew organically and is
+   disorganized.
+
+   helpful examples for using ltac are in the reference manual and in
+   "Logical Foundations: More Automation" *)
+
+(** * Tactics 
+
+    In most computations, we want to apply the top most substitution
+    to prove that a reduction holds. Writing all the correct terms is
+    a nuisance. We can use tactics to automate this process. *)
+
+(** First we apply the [n]-step patterns, and then use one step
+    reduction rules later. *)
+
+Ltac find_n_step_incr :=
+  match goal with
+  | |- n_step_reduces_to _ (app (lambda ?x) ?y) _ => apply n_step_incr with (u:=subst x 0 y)
+  | |- n_step_reduces_to _ (app ?x ?y) (app ?x ?z) => apply n_step_incr with (u:=app x z)
+  | |- n_step_reduces_to _ (app ?x ?z) (app ?y ?z) => apply n_step_incr with (u:=app y z)
+ end.
+
+Example find_n_step_sub :
+  n_step_reduces_to 1 (app (lambda (var 0)) (lambda (var 1))) (lambda (var 1)).
+Proof. find_n_step_incr. apply one_step_sub. simpl. apply n_step_refl. Qed.
+
+Example find_n_step_appl :
+  n_step_reduces_to 1 (app (app (lambda (var 0)) (lambda (var 1))) (var 2))
+    (app (lambda (var 1)) (var 2)).
+Proof.
+  find_n_step_incr. apply one_step_appl. apply one_step_sub.
+  apply n_step_refl.
+Qed.
+
+Example find_n_step_appr :
+  n_step_reduces_to 1 (app (var 2) (app (lambda (var 0)) (lambda (var 1))))
+    (app (var 2) (lambda (var 1))).
+Proof.
+  find_n_step_incr. apply one_step_appr. apply one_step_sub.
+  apply n_step_refl.
+Qed.
+
+Inductive opt {T: Type} : Type :=
+| None
+| Some (x: T).
+
+Fixpoint left_reduce_opt (s: term) :=
+  match s with
+  | var n => None
+  | app (lambda s) t => Some (subst s 0 t)
+  | app s t => match (left_reduce_opt s) with
+               | Some s' => Some (app s' t)                 
+               | None => match (left_reduce_opt t) with
+                         | None => None
+                         | Some t' => Some (app s t')
+                         end                           
+               end
+  | lambda s => match (left_reduce_opt s) with
+                | Some s' => Some (lambda s')
+                | None => None
+                end
+  end.
+
+Definition left_reduce (s: term) :=
+  match (left_reduce_opt s) with
+  | Some s' => s'
+  | None => s
+  end.
+
+Ltac find_n_step_naive :=
+  match goal with
+  | |- n_step_reduces_to _ ?x _ => apply n_step_incr with (u:=left_reduce x);
+                                   unfold left_reduce; simpl
+  end.
+
+(** After the [n]-step rule is applied, we use similar rules to prove
+    the one step reduction goals that are produced from the previous
+    tactic. *)
+
+Ltac find_one_step :=
+  match goal with
+  | |- one_step_reduces_to (app (lambda ?s) (lambda ?t)) _ => apply one_step_sub; simpl
+  | |- one_step_reduces_to (app ?x ?y) (app ?x ?z) => apply one_step_appr; simpl
+  | |- one_step_reduces_to (app ?x ?z) (app ?y ?z) => apply one_step_appl; simpl
+  end.
+
+(** * Examples 
+
+    Using the reduction rules defined above we can demonstrate some
+    properties of special combinators. *)
+
+(** ** False Returns Second of Two *)
+
+Lemma Fst_evaluates_iff_both_evaluate :
+  forall (s t: term), evaluates (app (app c_F s) t) <-> evaluates s /\ evaluates t.
+Proof.
+  intros s t. split.
+  - intros HFeval. inversion HFeval. inversion H.
+    + discriminate H0.
+    + split.
+      * inversion H2.
+        { discriminate H6. }
+        { unfold evaluates. exists v0. apply H9. }
+      * unfold evaluates. exists v. apply H3.
+  - intros [Hseval Hteval]. unfold evaluates.
+    unfold evaluates in Hseval. inversion Hseval as [s' Hs'].
+    unfold evaluates in Hteval. inversion Hteval as [t' Ht'].
+    exists t'.
+    apply eval with (s := (app c_F s)) (u := var 0)
+                    (t := t) (v := t').
+    apply eval with (s := c_F) (u := lambda (var 0))
+                    (t := s) (v := s').
+    apply refl with (u := lambda (var 0)).
+    reflexivity. reflexivity. apply Hs'. simpl.
+    apply refl with (u := var 0). reflexivity. reflexivity.
+    apply Ht'. simpl.
+    apply only_can_evaluate_to_abstr in Ht'.
+    unfold abstraction in Ht'. inversion Ht' as [u' Hu'].
+    apply refl with (u := u'). apply Hu'. apply Hu'.      
+Qed.
+
+(** ** Looping Does not Halt *)
+
+Lemma omega_omega_does_not_evaluate :
+  ~ evaluates (app c_omega c_omega).
+Proof.
+  (* It must be the case that the final evaluation is produced by a
+     substitution rule. In that case, it must be that - u = (app (var
+     0) (var 0)), and - v = lambda (app (var 0) (var 0)) = c_omega.
+     However, we see that (subst u 0 v) = c_omega, producing the
+     desired contradiction.
+
+     This was difficult because the (app c_omega c_omega) needs to be
+     generalized: we need to retain the information that s = (app
+     c_omega c_omega) to reach the contradiction. *)
+  unfold "~". unfold evaluates. intros Heval.  inversion Heval as [x Hx].
+  dependent induction Hx.
+  - assert (u = app (var 0) (var 0)) as Hudef.
+    { inversion Hx1. injection H0 as Hu0equ. injection H as Hu0def.
+      rewrite Hu0equ. rewrite Hu0def. reflexivity. }
+    assert (v = c_omega) as Hvdef.
+    { inversion Hx2. unfold c_omega. injection H as Hu0def.
+      rewrite H0. rewrite Hu0def. reflexivity. }
+    apply IHHx3. rewrite Hudef. rewrite Hvdef. simpl. reflexivity.
+Qed.
+
+(** ** Recursion Operator *)
+
+Definition c_C :=
+  lambda (lambda (app (var 0) (lambda (app (app (app (var 2) (var 2)) (var 1)) (var 0))))).
+
+Definition rho (s: term) :=
+  lambda (app (app (app c_C c_C) s) (var 0)).
+
+Lemma rho_is_recursive :
+  forall (u v: term),
+    combinator u -> combinator v ->
+    n_step_reduces_to 3 (app (rho u) v) (app (app u (rho u)) v).
+Proof.
+  intros u v. unfold combinator. unfold closed. unfold abstraction.
+  intros [Hubound Huabstr] [Hvbound Hvabstr].
+  inversion Huabstr as [u' Hu']. inversion Hvabstr as [v' Hv'].
+  unfold rho. rewrite Hu'. rewrite Hv'.
+  find_n_step_naive. find_one_step.
+  find_n_step_naive. find_one_step. find_one_step. find_one_step.
+  find_n_step_naive. find_one_step. find_one_step.
+  assert (forall (s: term), subst u' 1 s = u') as Hu'subst.
+  { intros s. rewrite Hu' in Hubound. simpl in Hubound.
+    apply bounds_block_subst with (k:=1). apply Hubound. }
+  rewrite Hu'subst. apply n_step_refl.
+Qed.
+
+Lemma rho_is_combinator_if_s_closed :
+  forall (s: term), closed s -> combinator (rho s).
+Proof.
+  unfold closed. intros s Hclosed.
+  unfold combinator. split.
+  unfold closed. simpl.
+  { split. split. lia.
+    apply bound_relaxes with (m:=0) (n:=1). auto. apply Hclosed.
+    auto. }
+  unfold rho. unfold abstraction.
+  exists (app (app (app c_C c_C) s) (var 0)). reflexivity.
+Qed.