From d19e67658ce87f49e6f47a11deb53de40df39e10 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Tue, 24 Oct 2023 16:27:57 +0200 Subject: [PATCH] My solutions to the warmup --- theories/type_systems/warmup/warmup.v | 177 +++++++++++++++++++++++--- 1 file changed, 156 insertions(+), 21 deletions(-) diff --git a/theories/type_systems/warmup/warmup.v b/theories/type_systems/warmup/warmup.v index 3f4f68b..12055dc 100644 --- a/theories/type_systems/warmup/warmup.v +++ b/theories/type_systems/warmup/warmup.v @@ -19,7 +19,13 @@ Inductive expr := (** Exercise 1: Arithmetics *) Fixpoint expr_eval (e : expr) : Z := (* TODO: write the function *) - 0. + match e with + | Const z => z + | Plus a b => (expr_eval a) + (expr_eval b) + | Mul a b => (expr_eval a) * (expr_eval b) + end. + +Check expr_eval (Mul (Const 3) (Const 2)). (** Now let's define some notation to make it look nice! *) (* We declare a so-called notation scope, so that we can still use the nice notations for addition on natural numbers [nat] and integers [Z]. *) @@ -41,22 +47,26 @@ Notation "e1 * e2" := (Mul e1%Z e2%Z) : expr. Lemma expr_eval_test: expr_eval (Plus (Const (-4)) (Const 5)) = 1%Z. Proof. - (* should be solved by: simpl. lia. *) - (* TODO: exercise *) -Admitted. + (* Apply the definition of expr_eval to the terms of the expression *) + simpl. + (* Use the linear algebra solver to finish the proof *) + lia. +Qed. Lemma plus_eval_comm e1 e2 : expr_eval (Plus e1 e2) = expr_eval (Plus e2 e1). Proof. - (* TODO: exercise *) -Admitted. + simpl. + rewrite Z.add_comm. + reflexivity. +Qed. Lemma plus_syntax_not_comm : Plus (Const 0) (Const 1) ≠ Plus (Const 1) (Const 0). Proof. - (* TODO: exercise *) -Admitted. + discriminate. +Qed. (** Exercise 2: Open arithmetical expressions *) @@ -70,6 +80,7 @@ Inductive expr' := | Plus' (e1 e2 : expr') | Mul' (e1 e2 : expr'). +(* Note: I have the habit of first defining these in Prop, before defining a function in bool if needed. I guess this makes more sense, though, as you ensure it is decidable *) (* We call an expression closed under the list X, if it only contains variables in X *) Fixpoint is_closed (X: list string) (e: expr') : bool := @@ -106,16 +117,38 @@ Qed. Lemma closed_mono X Y e: X ⊆ Y → closed X e → closed Y e. Proof. - unfold closed. intros Hsub; induction e as [ x | z | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2]; simpl. - - (* bool_decide is an stdpp function, which can be used to decide simple decidable propositions. - Make a search for it to find the right lemmas to complete this subgoal. *) - (* Search bool_decide. *) - admit. + unfold closed. + intros Hsub. + induction e as [ x | z | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2]. + simpl. + - + rewrite (bool_decide_eq_true (elem_of x X)). + rewrite (bool_decide_eq_true (elem_of x Y)). + auto. - done. - - (* Locate the notation for && by typing: Locate "&&". Then search for the right lemmas.*) - admit. - - admit. -Admitted. + - + simpl. + intro H. + rewrite andb_true_intro; auto. + split. + + rewrite IHe1; auto. + apply (andb_prop _ _ H). + + rewrite IHe2; auto. + apply (andb_prop _ _ H). + - + simpl. + intro H. + rewrite andb_true_intro; auto. + split. + + rewrite IHe1; auto. + apply (andb_prop _ _ H). + + rewrite IHe2; auto. + apply (andb_prop _ _ H). +Qed. (* we define a substitution operation on open expressions *) Fixpoint subst (e: expr') (x: string) (e': expr') : expr' := @@ -126,11 +159,77 @@ Fixpoint subst (e: expr') (x: string) (e': expr') : expr' := | Mul' e1 e2 => Mul' (subst e1 x e') (subst e2 x e') end. +Lemma closed_plus {e1 e2 X}: + closed X (Plus' e1 e2) -> (closed X e1) ∧ (closed X e2). +Proof. + intro H_closed. + (* Split H_closed into two hypotheses, one for `closed X e1` and one for `closewd X e2` *) + unfold closed in H_closed. + unfold is_closed in H_closed. + rewrite andb_true_iff in H_closed. + destruct H_closed as [H_closed_e1 H_closed_e2]. + + split. + assumption. + assumption. +Qed. + +Lemma closed_mul {e1 e2 X}: + closed X (Mul' e1 e2) -> (closed X e1) ∧ (closed X e2). +Proof. + intro H_closed. + (* Split H_closed into two hypotheses, one for `closed X e1` and one for `closewd X e2` *) + unfold closed in H_closed. + unfold is_closed in H_closed. + rewrite andb_true_iff in H_closed. + destruct H_closed as [H_closed_e1 H_closed_e2]. + + split. + assumption. + assumption. +Qed. + Lemma subst_closed e e' x X: closed X e → ¬ (x ∈ X) → subst e x e' = e. Proof. - (* TODO: exercise *) -Admitted. + intro H_closed. + intro H_x_free. + induction e as [ y | y | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2 ]. + simpl. + - rewrite <- decide_bool_decide. + rewrite decide_False. + auto. + intro H_eq. + (* Now we just need to prove a contradiction from x=y, x not in X, closed X (Var y) *) + unfold closed in H_closed. + unfold is_closed in H_closed. + rewrite H_eq in H_x_free. + rewrite (bool_decide_eq_true (y ∈ X)) in H_closed. + (* + Contradiction found: y ∈ X and y ∉ X; + NOTE: y ∉ X is syntax sugar for (y ∈ X) -> False + *) + exact (H_x_free H_closed). + - unfold subst; auto. + - + apply closed_plus in H_closed. + destruct H_closed as [H_closed_e1 H_closed_e2]. + simpl. + rewrite IHe1. + rewrite IHe2. + auto. + assumption. + assumption. + + - apply closed_mul in H_closed. + destruct H_closed as [H_closed_e1 H_closed_e2]. + simpl. + rewrite IHe1. + rewrite IHe2. + auto. + assumption. + assumption. +Qed. (* To evaluate an arithmetic expression, we define an evaluation function [expr_eval], which maps them to integers. @@ -145,10 +244,46 @@ Fixpoint expr_eval' (m: gmap string Z) (e : expr') : Z := | Mul' e1 e2 => (expr_eval' m e1) * (expr_eval' m e2) end. +(* + I do not know how to prove the following proof using constructive logic only. + One could probably do so by transforming the rhs + until they get to an equivalent expression to the lhs. +*) + +Require Import Classical_Prop. + (* Prove the following lemma which explains how substitution interacts with evaluation *) Lemma eval_subst_extend (m: gmap string Z) e x e': expr_eval' m (subst e x e') = expr_eval' (<[x := expr_eval' m e']> m) e. Proof. - (* TODO: exercise *) -Admitted. + induction e as [ y | y | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2 ]. + - + simpl. + destruct (classic (x = y)) as [H_eq | H_neq]. + (* If x = y *) + rewrite <- decide_bool_decide; rewrite decide_True. + rewrite H_eq. + rewrite lookup_insert. + unfold default. + simpl. + reflexivity. + assumption. + (* If x ≠ y *) + rewrite <- decide_bool_decide; rewrite decide_False; simpl. + rewrite lookup_insert_ne. + reflexivity. + assumption. + assumption. + - auto. + - + simpl. + rewrite IHe1. + rewrite IHe2. + reflexivity. + - + simpl. + rewrite IHe1. + rewrite IHe2. + reflexivity. +Qed.