@ -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 *)
Admitt .
discriminate .
Q .
(* * 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 .
