path: root/theories/Evaluation.v

(* 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.