(*| ============================================ Week 7: Simply-Typed Lambda Calculus (STLC) ============================================ :status: hidden Author `Adam Chlipala `__, `Benjamin C. Pierce `__ `Aurèle Barrière `__, License No redistribution allowed (usage by permission in CS-428). .. contents:: .. coq:: none |*) Require Import String. Open Scope string_scope. (*| Introduction ============ The last few chapters have focused on small programming languages that are representative of the essence of the imperative languages. We now turn to lambda-calculus, the usual representative of functional languages. |*) Notation var := string. Definition var_eq : forall x y : var, {x = y} + {x <> y} := string_dec. Infix "==v" := var_eq (no associativity, at level 50). (*| The simply typed lambda-calculus (STLC) is a tiny core calculus embodying the key concept of functional abstraction. This concept shows up in pretty much every real-world programming language in some form (functions, procedures, methods, etc.). We will follow a standard pattern: we formalize the calculus (syntax, small-step semantics), we define the typing rules, and finally we prove interesting properties about the type system (progress and preservation). The new technical challenges arise from the mechanisms of variable binding and substitution. It will take some work to deal with these. |*) Module Stlc. (*| Syntax ====== In our version of STLC, we have natural number constants and addition. This will let us define a simple type systems that checks whether something evaluates to a natural number. If you are used to a simpler definition of Lambda calculus, we will see as exercises how to encode natural numbers using the more basic lambda calculus. |*) Inductive exp : Set := | Var (x : var) | Const (n : nat) | Plus (e1 e2 : exp) | Abs (x : var) (e1 : exp) | App (e1 e2 : exp). (*| The STLC is a language of higher-order functions: we can write down functions that take other functions as arguments and/or return other functions as results. The STLC doesn't provide any primitive syntax for defining named functions: i.e., all functions are "anonymous." But they could easily be introduced: indeed, the fundamental naming and binding mechanisms are exactly the same. The STLC lives in the lower-left front corner of the famous lambda cube (also called the Barendregt Cube), which visualizes three sets of features that can be added to its simple core: |*) (* Calculus of Constructions type operators +--------+ /| /| / | / | polymorphism +--------+ | | | | | | +-----|--+ | / | / |/ |/ +--------+ dependent types STLC *) (*| Moving from bottom to top in the cube corresponds to adding polymorphic types like `forall X, X -> X`. Adding just polymorphism gives us the famous Girard-Reynolds calculus, System F. (terms bind types) Moving from front to back corresponds to adding type operators like `list`. (types bind types) Moving from left to right corresponds to adding dependent types like `forall n, array-of-size n`. (types bind terms) The top right corner on the back, which combines all three features, is called the Calculus of Constructions. First studied by Coquand and Huet, it forms the foundation of Coq's logic. Coq's logic is the Calculus of Inductive Constructions (CIC), a variant of the Calculus of COnstructions. Semantics ========= To define the small-step semantics of STLC terms, we begin, as always, by defining the set of values. Next, we define the critical notion of substitution, which is used in the reduction rule for application expressions. And finally we give the small-step relation itself. |*) Inductive value : exp -> Prop := | VConst : forall n, value (Const n) | VAbs : forall x e1, value (Abs x e1). (*| Recall that value correspond to terms that have no more work to do. Clearly, constants are value, and applications are not. For abstractions, we have a choice: - We can say that `\x.t` is a value only when `t` is a value -- i.e., only if the function's body has been reduced (as much as it can be without knowing what argument it is going to be applied to). - Or we can say that `\x.t` is always a value, no matter whether `t` is one or not -- in other words, we can say that reduction stops at abstractions. Our usual way of evaluating expressions in Gallina makes the first choice -- for example, |*) Compute (fun x:bool => 3 + 4). (*| But Gallina is rather unusual in this respect. Most real-world functional programming languages make the second choice -- reduction of a function's body only begins when the function is actually applied to an argument. We also make the second choice here. Now we come to the heart of the STLC: the operation of substituting one term for a variable in another term. This operation is used below to define the operational semantics of function application, where we will need to substitute the argument term for the function parameter in the function's body. Here `subst e1 x e2` replaces all occurences of `x` in `e2` with `e1`. Here we define a functional version, but we could very well have defined an inductive proposition. `subst` is not applicable when `e1` is not closed, to avoid some complexity we don't need. |*) Fixpoint subst (e1 : exp) (x : string) (e2 : exp) : exp := match e2 with | Var y => if y ==v x then e1 else Var y | Const n => Const n | Plus e2' e2'' => Plus (subst e1 x e2') (subst e1 x e2'') | Abs y e2' => Abs y (if y ==v x then e2' else subst e1 x e2') | App e2' e2'' => App (subst e1 x e2') (subst e1 x e2'') end. Inductive step : exp -> exp -> Prop := (* These rules show the real action of the semantics. *) | Beta : forall x e v, value v -> step (App (Abs x e) v) (subst v x e) | Add : forall n1 n2, step (Plus (Const n1) (Const n2)) (Const (n1 + n2)) (* Then we have a bunch of bureaucratic, repetitive rules encoding evaluation order. See next lecture for how to streamline this part, but for now note that the [value] premises below are crucial to enforce a single order of evaluation. *) | App1 : forall e1 e1' e2, step e1 e1' -> step (App e1 e2) (App e1' e2) | App2 : forall v e2 e2', value v -> step e2 e2' -> step (App v e2) (App v e2') | Plus1 : forall e1 e1' e2, step e1 e1' -> step (Plus e1 e2) (Plus e1' e2) | Plus2 : forall v e2 e2', value v -> step e2 e2' -> step (Plus v e2) (Plus v e2'). (*| Some helpful notations to define programs. |*) Coercion Const : nat >-> exp. Infix "^+^" := Plus (at level 50). Coercion Var : var >-> exp. Notation "\ x , e" := (Abs x e) (at level 51). Infix "@" := App (at level 49, left associativity). (*| Believe it or not, this is a Turing-complete language! Here's an example nonterminating program. |*) Check "x". Example omega := (\"x", "x" @ "x") @ (\"x", "x" @ "x"). Lemma omega_loop: step omega omega. Proof. constructor. constructor. Qed. (*| Types and Typing Environments ============================= That language is suitable to describe with a static *type system*. Here's our modest, but countably infinite, set of types. |*) Inductive type := | Nat (* Numbers *) | Fun (dom ran : type) (* Functions *). (*| Although we are primarily interested in the binary relation relating a closed term `t` to its type `T`, we need to generalize a bit to make the definitions work. Consider checking that `\a,tb` has type `TA->TB`. Intuitively, we need to check that `tb` has type `TB`. However, we have removed the binder `\a`, so `a` may occur free in `tb` (that is, `tb` may be open). While checking that `tb` has type `TB`, we must remember that `a` has type `TA`, in order to deal with these free occurrences of `a`. Similarly, `tb` itself could contain abstractions, and typechecking their bodies could require looking up the declared types of yet more free variables. To keep track of all this, we add a third element to the relation, a typing context, which records the types of the variables that may occur free in a term -- that is, a partial map from variables to types. Let us write these type maps and their operations. |*) Definition type_map: Type := var -> option type. Definition empty_map : type_map := (fun v => None). Notation "$0" := empty_map. Definition tmap_get (tm:type_map) (v:var): option type := tm v. Infix "$?" := tmap_get (no associativity, at level 50). Definition tmap_set (tm:type_map) (vt:var * type) := fun v => if (v ==v fst vt) then Some (snd vt) else tm v. Infix "$+" := tmap_set (no associativity, at level 50). Lemma tmap_gss: forall tm v t, (tm $+ (v,t)) $? v = Some t. Proof. intros tm v t. unfold tmap_get, tmap_set. simpl. unfold var_eq. destruct (string_dec v v); auto. exfalso. apply n. auto. Qed. Lemma tmap_gso: forall tm v1 v2 t, v1 <> v2 -> (tm $+ (v1,t)) $? v2 = tm $? v2. Proof. intros tm v1 v2 t H. unfold tmap_get, tmap_set. simpl. unfold var_eq. destruct (string_dec v2 v1); auto. exfalso. apply H. auto. Qed. Lemma tmap_shadow: forall tm v t1 t2 v', ((tm $+ (v, t1)) $+ (v, t2)) $? v' = (tm $+ (v, t2)) $? v'. Proof. intros tm v t1 t2 v'. destruct (v' ==v v). + subst. repeat rewrite tmap_gss. auto. + repeat (rewrite tmap_gso; auto). Qed. Lemma tmap_permute: forall tm v1 t1 v2 t2 v', v1 <> v2 -> ((tm $+ (v1, t1)) $+ (v2, t2)) $? v' = ((tm $+ (v2, t2)) $+ (v1, t1)) $? v'. Proof. intros tm v1 t1 v2 t2 v' H. destruct (v' ==v v1); destruct (v' ==v v2); subst. - exfalso. apply H. auto. - rewrite tmap_gss. rewrite tmap_gso; auto. apply tmap_gss. - rewrite tmap_gss. rewrite tmap_gso; auto. symmetry. apply tmap_gss. - repeat (rewrite tmap_gso; auto). Qed. (*| In one proof later, it will be convenient to talk about typing contexts being equal if they just map each variable to the same type option. But take the lemma above: although the two maps return the value for any var `v'`, the two functions are not equal in the sense of Coq equality. Ley's make a quick detour through functional extensionality. |*) Module Ext. (*| Functional Extensionality ========================= Coq's logic is quite minimalistic. This means that one occasionally encounters cases where translating standard mathematical reasoning into Coq is cumbersome -- or even impossible -- unless we enrich its core logic with additional axioms. For example, the equality assertions that we have seen so far mostly have concerned elements of inductive types (nat, bool, etc.). But, since Coq's equality operator is polymorphic, we can use it at _any_ type -- in particular, we can write propositions claiming that two _functions_ are equal to each other: |*) Example function_equality_ex1 : (fun x => 3 + x) = (fun x => (pred 4) + x). Proof. reflexivity. Qed. (*| These two functions are equal just by simplification, but in general functions can be equal for more interesting reasons. In common mathematical practice, two functions are considered equal if they produce the same output on every input: This is known as the principle of functional extensionality. Informally, an "extensional property" is one that pertains to an object's observable behavior. Thus, functional extensionality simply means that a function's identity is completely determined by what we can observe from it -- i.e., the results we obtain after applying it. However, functional extensionality is not part of Coq's built-in logic. This means that some intuitively obvious propositions are not provable. |*) Example function_equality_ex2 : (fun x => plus x 1) = (fun x => plus 1 x). Proof. simpl. Fail rewrite PeanoNat.Nat.add_comm. Abort. (*| However, if we like, we can add functional extensionality to Coq's core using the `Axiom` command. |*) Axiom functional_extensionality : forall {X Y: Type} {f g : X -> Y}, (forall (x:X), f x = g x) -> f = g. (*| Defining something as an `Axiom` has the same effect as stating a theorem and skipping its proof using `Admitted`, but it alerts the reader that this isn't just something we're going to come back and fill in later! We can now invoke functional extensionality in proofs: |*) Example function_equality_ex2 : (fun x => x + 1) = (fun x => 1 + x). Proof. apply functional_extensionality. intros x. apply PeanoNat.Nat.add_comm. Qed. (*| Coq provides a nice way to see on which axioms, parameters and admitted proofs each of your theorems depend on. For instance, it can show that the theorem `function_equality_ex2` only depends on the functional extensionality axiom. |*) Print Assumptions function_equality_ex2. (*| Naturally, we need to be quite careful when adding new axioms into Coq's logic, as this can render it inconsistent -- that is, it may become possible to prove every proposition, including False, 2+2=5, etc.! In general, there is no simple way of telling whether an axiom is safe to add: hard work by highly trained mathematicians is often required to establish the consistency of any particular combination of axioms. Fortunately, it is known that adding functional extensionality, in particular, is consistent. For this reason, it's available in the standard library (`Logic.FunctionalExtensionality `_). Other examples of known consistent axioms include the functional axiom of choice and proof irrelevance. See more details here https://github.com/coq/coq/wiki/The-Logic-of-Coq#axioms. |*) End Ext. From Coq Require Import Logic.FunctionalExtensionality. Lemma tmap_permute_ext: forall tm v1 t1 v2 t2, v1 <> v2 -> (tm $+ (v1, t1)) $+ (v2, t2) = (tm $+ (v2, t2)) $+ (v1, t1). Proof. intros tm v1 t1 v2 t2 H. apply functional_extensionality. intros x. pose proof (tmap_permute tm v1 t1 v2 t2). unfold tmap_get in H0. auto. Qed. (*| Typing System ============= |*) Inductive has_ty : type_map -> exp -> type -> Prop := | HtVar : forall G x t, G $? x = Some t -> has_ty G (Var x) t | HtConst : forall G n, has_ty G (Const n) Nat | HtPlus : forall G e1 e2, has_ty G e1 Nat -> has_ty G e2 Nat -> has_ty G (Plus e1 e2) Nat | HtAbs : forall G x e1 t1 t2, has_ty (G $+ (x, t1)) e1 t2 -> has_ty G (Abs x e1) (Fun t1 t2) | HtApp : forall G e1 e2 t1 t2, has_ty G e1 (Fun t1 t2) -> has_ty G e2 t1 -> has_ty G (App e1 e2) t2. Local Hint Constructors value step has_ty : core. (* some notation for the typing judgement *) Notation "Gamma '|--' e '\in' T" := (has_ty Gamma e T) (at level 101). Infix "-->" := Fun (at level 60, right associativity). (* Some examples of typed programs *) Example one_plus_one : $0 |-- (1 ^+^ 1) \in Nat. Proof. eauto. Qed. Example add : $0 |-- (\"n", \"m", "n" ^+^ "m") \in (Nat --> Nat --> Nat). Proof. repeat (econstructor; simpl). Qed. Example eleven : $0 |-- ((\"n", \"m", "n" ^+^ "m") @ 7 @ 4) \in Nat. Proof. repeat (econstructor; simpl). Qed. Example seven_the_long_way : $0 |-- ((\"x", "x") @ (\"x", "x") @ 7) \in Nat. Proof. repeat (econstructor; simpl). Qed. (*| Type Soundness ============== What useful invariants could we prove about programs in this language? How about that, at every point, either they're finished executing or they can take further steps? For instance, a program that tried to add a function to a number would not satisfy that condition, and we call it *stuck*. We want to prove that typed programs can never become stuck. Here's a good invariant to strive for. |*) Definition unstuck e := value e \/ (exists e' : exp, step e e'). (*| We can now define some useful lemmas about typed values. |*) Lemma val_nat: forall e, ($0 |-- e \in Nat) -> value e -> exists n, e = Const n. Proof. intros e H H0. inversion H0; subst; inversion H; subst. eauto. Qed. Lemma val_fun: forall e t1 t2, ($0 |-- e \in (t1 --> t2)) -> value e -> exists x u, e = \x, u. Proof. intros e t1 t2 H H0. inversion H0; subst; inversion H; subst. eauto. Qed. (*| The progress theorem tells us that closed, well-typed terms are not stuck: either a well-typed term is a value, or it can take a reduction step. |*) Lemma progress : forall e t, ($0 |-- e \in t) -> unstuck e. Proof. intros e t H. remember empty_map as Gamma. unfold unstuck. assert ($0 = $0) by auto. induction H; subst G; auto. - unfold empty_map, tmap_get in H. inversion H. - right. specialize (IHhas_ty1 H0). specialize (IHhas_ty2 H0). destruct IHhas_ty1. 2: { destruct H2. eexists. apply Plus1; eauto. } destruct IHhas_ty2. + specialize (val_nat e1 H H2) as [n1 He1]. specialize (val_nat e2 H1 H3) as [n2 He2]. subst. eexists. apply Add. + specialize (val_nat e1 H H2) as [n1 He1]. subst. destruct H3. eexists. apply Plus2; eauto. - right. specialize (IHhas_ty1 H0). specialize (IHhas_ty2 H0). destruct IHhas_ty1. 2: { destruct H2. eexists. apply App1; eauto. } destruct IHhas_ty2. + specialize (val_fun e1 _ _ H H2) as [x1 [u1 Hf1]]. subst. eexists. apply Beta; auto. + destruct H3. eexists. apply App2; eauto. Qed. (*| This could also be proved by induction on `e` (left as exercise). The other half of the type soundness property is the preservation of types during reduction. For this part, we'll need to develop some technical machinery for reasoning about variables and substitution. Working from top to bottom (from the high-level property we are actually interested in to the lowest-level technical lemmas that are needed by various cases of the more interesting proofs), the story goes like this: - The preservation theorem is proved by induction on a typing derivation. There is one interesting case: the Beta-reduction. Its definition uses the substitution operation. To see that this step preserves typing, we need to know that the substitution itself does. So we prove a... - substitution lemma, stating that substituting a (well-typed) term for a variable in a term preserves the type of the term. The proof requires looking at all the different cases in the definition of substitition. This time, for the variables case, we discover that we need to deduce from the fact that a term `x` has type `T` in the empty context the fact that `x` has type `T` in every context. For this we prove a... - weakening lemma, showing that typing is preserved under "extensions" to the typing context. To make Coq happy, of course, we need to formalize the story in the opposite order, starting with weakening... Inclusion between typing contexts is preserved by adding the same new mapping to both. |*) Lemma weakening_override : forall (G G' : type_map) x t, (forall x' t', G $? x' = Some t' -> G' $? x' = Some t') -> (forall x' t', G $+ (x, t) $? x' = Some t' -> G' $+ (x, t) $? x' = Some t'). Proof. intros G G' x t H x' t' H0. destruct (x ==v x'); simpl. - subst. rewrite tmap_gss. rewrite tmap_gss in H0. auto. - rewrite tmap_gso; auto. rewrite tmap_gso in H0; auto. Qed. (*| This lemma lets us propagate a typing derivation into a new context that includes the old one. |*) Lemma weakening : forall G e t, (G |-- e \in t) -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t) -> G' |-- e \in t. Proof. intros G e t H. induction H; intros. - apply H0 in H. constructor. auto. - constructor. - constructor; auto. - constructor. apply IHhas_ty. apply weakening_override. auto. - econstructor; auto. Qed. Corollary empty_weakening: forall tm e t, ($0 |-- e \in t) -> tm |-- e \in t. Proof. intros tm e t H. eapply weakening; eauto. intros x t0 H0. unfold empty_map, tmap_get in H0. inversion H0. Qed. (*| Replacing a variable with a properly typed term preserves typing. |*) Lemma substitution : forall G x t' e t e', ((G $+ (x, t')) |-- e \in t) -> ($0 |-- e' \in t') -> G |-- (subst e' x e) \in t. Proof. intros G x t' e t e' H. remember (G $+ (x, t')) as G'. generalize dependent G. induction H; intros; simpl; eauto; subst. - destruct (x0 ==v x). + subst. rewrite tmap_gss in H. inversion H. subst. eapply empty_weakening; eauto. + rewrite tmap_gso in H; auto. - destruct (x0 ==v x). + subst. constructor. eapply weakening; eauto. intros x0 t H1. rewrite tmap_shadow in H1. auto. + apply HtAbs. apply IHhas_ty; auto. apply functional_extensionality. intros x1. rewrite tmap_permute_ext; auto. Qed. (*| The actual preservation lemma: |*) Lemma preservation : forall e1 e2, step e1 e2 -> forall t, ($0 |-- e1 \in t) -> $0 |-- e2 \in t. Proof. intros e1 e2 H. remember empty_map as Gamma. induction H; intros; simpl; subst. 2-6: match goal with | [ H: has_ty _ _ _ |- _ ] => inversion H; subst; econstructor; eauto end. inversion H0; subst. inversion H4; subst. eapply substitution; eauto. Qed. (*| Multi-step Soundness ==================== Putting progress and preservation together, we see that a well-typed term can never reach a stuck state. |*) Inductive trc {A:Type} {R:A -> A -> Prop}: A -> A -> Prop := | TrcRefl : forall x, trc x x | TrcFront : forall x y z (STEP: R x y) (STAR: trc y z), trc x z. Local Hint Resolve TrcRefl TrcFront : core. Notation "R ^*" := (@trc _ R) (at level 0). Corollary multi_step_soundness : forall t t' T, ($0 |-- t \in T) -> step^* t t' -> unstuck t'. Proof. intros t t' T HT P. induction P. - apply progress in HT. auto. - apply IHP. eapply preservation; eauto. Qed. (*| Subject Expansion ================= The preservation theorem is often called subject reduction, because it tells us what happens when the "subject" of the typing relation is reduced. Another property of some type systems is called Subject Expansion. Informally, it means that, if `t` steps to `t'` and `$0 |-- t' \in T`, then `$0 |-- t \in T`. Is that the case for STLC? |*) Theorem not_subject_expansion: exists t t' T, step t t' /\ ($0 |-- t' \in T) /\ ~ ($0 |-- t \in T). Proof. exists ((\"x", 0) @ (\"y", 0 @ 1)). exists (0). exists Nat. repeat split. - constructor. constructor. - constructor. - unfold not. intros H. inversion H; subst. inversion H5; subst. inversion H6; subst. inversion H4; subst. Qed. End Stlc. (*| We now go back to untyped lambda calculus without natural numbers and prove that we can encode natural numbers. |*) Module Ulc. Inductive exp : Set := | Var (x : var) | Abs (x : var) (body : exp) | App (e1 e2 : exp). Fixpoint subst (rep : exp) (x : var) (e : exp) : exp := match e with | Var y => if y ==v x then rep else Var y | Abs y e1 => Abs y (if y ==v x then e1 else subst rep x e1) | App e1 e2 => App (subst rep x e1) (subst rep x e2) end. (*| This time, for a change, we'll define big-step semantics. |*) Inductive eval : exp -> exp -> Prop := | BigAbs : forall x e, eval (Abs x e) (Abs x e) | BigApp : forall e1 x e1' e2 v2 v, eval e1 (Abs x e1') -> eval e2 v2 -> eval (subst v2 x e1') v -> eval (App e1 e2) v. (*| Note that we omit a `Var` case, since variable terms can't be *closed*, and therefore they aren't meaningful as top-level programs. |*) Inductive value : exp -> Prop := | Value : forall x e, value (Abs x e). Local Hint Constructors eval value : core. (*| Every value executes to itself, and `eval` only produces values. |*) Theorem value_eval : forall v, value v -> eval v v. Proof. intros v H. inversion H. auto. Qed. Local Hint Resolve value_eval : core. Theorem eval_value : forall e v, eval e v -> value v. Proof. intros e v H. induction H; auto. Qed. Local Hint Resolve eval_value : core. Coercion Var : var >-> exp. Notation "\ x , e" := (Abs x e) (at level 50). Infix "@" := App (at level 49, left associativity). (*| Church numerals =============== Here are two curious definitions. |*) Definition zero := \"f", \"x", "x". Definition plus1 := \"n", \"f", \"x", "f" @ ("n" @ "f" @ "x"). (*| We can build up any natural number `n` as `plus1^n @ zero`. Let's prove that, in fact, these definitions constitute a workable embedding of the natural numbers in lambda-calculus. A term `plus^n @ zero` evaluates to something very close to what this function returns. |*) Fixpoint canonical' (n : nat) : exp := match n with | O => "x" | S n' => "f" @ ((\"f", \"x", canonical' n') @ "f" @ "x") end. (*| This missing piece is this wrapper. |*) Definition canonical n := \"f", \"x", canonical' n. (*| .. exercise:: Represents Let's formalize our definition of what it means to represent a number. |*) Definition represents (e : exp) (n : nat) := eval e (canonical n). Theorem zero_ok : represents zero 0. (*| .. solution:: .. coq:: |*) Proof. unfold zero, represents, canonical. simpl. econstructor. Qed. (*| .. coq:: |*) Theorem plus1_ok : forall e n, represents e n -> represents (plus1 @ e) (S n). (*| .. solution :: .. coq:: |*) Proof. unfold plus1, represents, canonical; simpl. econstructor. econstructor. eassumption. simpl. econstructor. Qed. (*| .. exercise:: add What's basically going on here? The representation of number `n` is `N` such that, for any function `f`: `N(f) = f^n`. That is, we represent a number as its repeated-composition operator. So, given a number, we can use it to repeat any operation. In particular, to implement addition, we can just repeat `plus1`! |*) Definition add := \"n", \"m", "n" @ plus1 @ "m". Example add_1_2 : exists v, eval (add @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero))) v /\ eval (plus1 @ (plus1 @ (plus1 @ zero))) v. (*| .. solution:: .. coq:: |*) Proof. eexists; split. repeat (econstructor; simpl). repeat econstructor. Qed. (*| .. exercise:: Substitution of `m` By the way: since `canonical'` doesn't mention variable `m`, substituting for `m` has no effect. This fact will come in handy shortly. |*) Lemma subst_m_canonical' : forall n m, subst m "m" (canonical' n) = canonical' n. (*| .. solution:: .. coq:: |*) Proof. intros n. induction n; intros; simpl; auto. rewrite IHn. auto. Qed. (*| .. exercise:: `add_ok` This inductive proof is the workhorse for the next result, so let's skip ahead there. |*) Lemma add_ok' : forall n m, eval (subst (\ "f", (\ "x", canonical' m)) "x" (subst (\ "n", (\ "f", (\ "x", "f" @ (("n" @ "f") @ "x")))) "f" (canonical' n))) (canonical (n + m)). (*| .. solution:: .. coq:: |*) Proof. intros n. induction n; simpl; auto. econstructor; eauto. - econstructor; eauto. econstructor; eauto. - simpl. econstructor. Qed. (*| .. coq:: |*) Theorem add_ok : forall n ne m me, represents ne n -> represents me m -> represents (add @ ne @ me) (n + m). (*| .. solution:: .. coq:: |*) Proof. unfold represents; simpl. intros n ne m me H H0. econstructor; eauto. - econstructor; eauto. + econstructor; eauto. + econstructor; eauto. - simpl. econstructor; eauto. 2: apply add_ok'. econstructor; eauto. rewrite subst_m_canonical'. econstructor; eauto. Qed. (*| .. exercise:: `mult_ok` Let's repeat the same exercise for multiplication. |*) Definition mult := \"n", \"m", "n" @ (add @ "m") @ zero. Example mult_1_2 : exists v, eval (mult @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero))) v /\ eval (plus1 @ (plus1 @ zero)) v. (*| .. solution:: .. coq:: |*) Proof. eexists; split. - repeat (econstructor; simpl). - repeat econstructor. Qed. (*| .. coq:: |*) Lemma mult_ok' : forall n m, eval (subst (\ "f", (\ "x", "x")) "x" (subst (\ "m", ((\ "f", (\ "x", canonical' m)) @ (\ "n", (\ "f", (\ "x", "f" @ (("n" @ "f") @ "x"))))) @ "m") "f" (canonical' n))) (canonical (n * m)). (*| .. solution:: .. coq:: |*) Proof. intros n. induction n; intros; simpl. { auto. } econstructor; eauto. { repeat (econstructor; eauto). } econstructor; simpl; eauto. 2: { apply add_ok'. } econstructor; eauto. simpl. rewrite subst_m_canonical'. econstructor; eauto. Qed. (*| .. coq:: |*) Theorem mult_ok : forall n ne m me, represents ne n -> represents me m -> represents (mult @ ne @ me) (n * m). (*| .. solution:: .. coq:: |*) Proof. unfold represents; simpl. econstructor; eauto. - econstructor; eauto. { econstructor; eauto. } econstructor; eauto. - simpl. econstructor; eauto. 2:{ apply mult_ok'. } econstructor; eauto. 2:{ simpl. rewrite subst_m_canonical'. econstructor; eauto. } econstructor; eauto. Qed. End Ulc.