diff options
Diffstat (limited to 'theories/Evaluation.v')
| -rw-r--r-- | theories/Evaluation.v | 553 |
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. |