(* week-12_observational-equivalence_the-live-proving-session.v *) (* Version of 11 Apr 2025 *) (* was: *) (* week-12_observational-equivalence.v *) (* LPP 2025 - CS3234 2024-2025, Sem2 *) (* Olivier Danvy *) (* Version of 11 Apr 2025 *) (* ********** *) Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity. Require Import Bool Arith List String. Definition String_eqb (s1 s2 : string) : bool := match String.string_dec s1 s2 with left _ => true | right _ => false end. (* ********** *) (* Names: *) Definition name : Type := string. (* ***** *) (* The abstract data type of environments: *) Definition environment (denotable : Type) : Type := list (name * denotable). Definition mt (denotable : Type) : environment denotable := nil. Definition extend (denotable : Type) (x : name) (d : denotable) (e : environment denotable) : environment denotable := (x , d) :: e. Fixpoint lookup (denotable : Type) (x : name) (e : environment denotable) : option denotable := match e with nil => None | (x', d) :: e' => if String_eqb x x' then Some d else lookup denotable x e' end. Lemma fold_unfold_lookup_nil : forall (denotable : Type) (x : name), lookup denotable x nil = None. Proof. fold_unfold_tactic lookup. Qed. Lemma fold_unfold_lookup_cons : forall (denotable : Type) (x x' : name) (d : denotable) (e' : environment denotable), lookup denotable x ((x', d) :: e') = if String_eqb x x' then Some d else lookup denotable x e'. Proof. fold_unfold_tactic lookup. Qed. (* ********** *) (* Syntax: *) Inductive arithmetic_expression : Type := Literal : nat -> arithmetic_expression | Name : name -> arithmetic_expression | Plus : arithmetic_expression -> arithmetic_expression -> arithmetic_expression | Times : arithmetic_expression -> arithmetic_expression -> arithmetic_expression. (* ********** *) (* Semantics: *) Inductive msg : Type := Undeclared_name : name -> msg. Inductive expressible_value : Type := Expressible_nat : nat -> expressible_value | Expressible_msg : msg -> expressible_value. (* ********** *) Definition specification_of_evaluate_ltr (evaluate : arithmetic_expression -> environment nat -> expressible_value) := (forall (n : nat) (e : environment nat), evaluate (Literal n) e = Expressible_nat n) /\ ((forall (x : string) (e : environment nat) (n : nat), lookup nat x e = Some n -> evaluate (Name x) e = Expressible_nat n) /\ (forall (x : string) (e : environment nat), lookup nat x e = None -> evaluate (Name x) e = Expressible_msg (Undeclared_name x))) /\ ((forall (ae1 ae2 : arithmetic_expression) (e : environment nat) (n1 n2 : nat), evaluate ae1 e = Expressible_nat n1 -> evaluate ae2 e = Expressible_nat n2 -> evaluate (Plus ae1 ae2) e = Expressible_nat (n1 + n2)) /\ (forall (ae1 ae2 : arithmetic_expression) (e : environment nat) (n1 : nat) (m2 : msg), evaluate ae1 e = Expressible_nat n1 -> evaluate ae2 e = Expressible_msg m2 -> evaluate (Plus ae1 ae2) e = Expressible_msg m2) /\ (forall (ae1 ae2 : arithmetic_expression) (e : environment nat) (m1 : msg), evaluate ae1 e = Expressible_msg m1 -> evaluate (Plus ae1 ae2) e = Expressible_msg m1)) /\ ((forall (ae1 ae2 : arithmetic_expression) (e : environment nat) (n1 n2 : nat), evaluate ae1 e = Expressible_nat n1 -> evaluate ae2 e = Expressible_nat n2 -> evaluate (Times ae1 ae2) e = Expressible_nat (n1 * n2)) /\ (forall (ae1 ae2 : arithmetic_expression) (e : environment nat) (n1 : nat) (m2 : msg), evaluate ae1 e = Expressible_nat n1 -> evaluate ae2 e = Expressible_msg m2 -> evaluate (Times ae1 ae2) e = Expressible_msg m2) /\ (forall (ae1 ae2 : arithmetic_expression) (e : environment nat) (m1 : msg), evaluate ae1 e = Expressible_msg m1 -> evaluate (Times ae1 ae2) e = Expressible_msg m1)). (* ********** *) Definition specification_of_evaluate_rtl (evaluate : arithmetic_expression -> environment nat -> expressible_value) := (forall (n : nat) (e : environment nat), evaluate (Literal n) e = Expressible_nat n) /\ ((forall (x : string) (e : environment nat) (n : nat), lookup nat x e = Some n -> evaluate (Name x) e = Expressible_nat n) /\ (forall (x : string) (e : environment nat), lookup nat x e = None -> evaluate (Name x) e = Expressible_msg (Undeclared_name x))) /\ ((forall (ae1 ae2 : arithmetic_expression) (e : environment nat) (n2 n1 : nat), evaluate ae2 e = Expressible_nat n2 -> evaluate ae1 e = Expressible_nat n1 -> evaluate (Plus ae1 ae2) e = Expressible_nat (n1 + n2)) /\ (forall (ae1 ae2 : arithmetic_expression) (e : environment nat) (n2 : nat) (m1 : msg), evaluate ae2 e = Expressible_nat n2 -> evaluate ae1 e = Expressible_msg m1 -> evaluate (Plus ae1 ae2) e = Expressible_msg m1) /\ (forall (ae1 ae2 : arithmetic_expression) (e : environment nat) (m2 : msg), evaluate ae2 e = Expressible_msg m2 -> evaluate (Plus ae1 ae2) e = Expressible_msg m2)) /\ ((forall (ae1 ae2 : arithmetic_expression) (e : environment nat) (n2 n1 : nat), evaluate ae2 e = Expressible_nat n2 -> evaluate ae1 e = Expressible_nat n1 -> evaluate (Times ae1 ae2) e = Expressible_nat (n1 + n2)) /\ (forall (ae1 ae2 : arithmetic_expression) (e : environment nat) (n2 : nat) (m1 : msg), evaluate ae2 e = Expressible_nat n2 -> evaluate ae1 e = Expressible_msg m1 -> evaluate (Times ae1 ae2) e = Expressible_msg m1) /\ (forall (ae1 ae2 : arithmetic_expression) (e : environment nat) (m2 : msg), evaluate ae2 e = Expressible_msg m2 -> evaluate (Times ae1 ae2) e = Expressible_msg m2)). (* ********** *) (* Exercise 07a, with a solution *) Proposition Literal_0_is_neutral_for_Plus_on_the_left_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae2 : arithmetic_expression) (e : environment nat), evaluate (Plus (Literal 0) ae2) e = evaluate ae2 e. Proof. intros evaluate [S_evaluate_Literal [[S_evaluate_Name_n S_evaluate_Name_m] [[S_evaluate_Plus_nn [S_evaluate_Plus_nm S_evaluate_Plus_m]] [S_evaluate_Times_nn [S_evaluate_Times_nm S_evaluate_Times_m]]]]] ae2 e. (* See how each of the components in the specification is named? *) (* But only a few of them are needed to prove this proposition. *) (* So let us delay their naming to those that are needed in each case. *) Restart. intros evaluate S_evaluate ae2 e. case (evaluate ae2 e) as [n2 | m2] eqn:E_ae2. - destruct S_evaluate as [S_evaluate_Literal [_ [[S_evaluate_Plus_nn [_ _]] _]]]. Check (S_evaluate_Plus_nn (Literal 0) ae2 e). Check (S_evaluate_Plus_nn (Literal 0) ae2 e 0 n2). Check (S_evaluate_Literal 0 e). Check (S_evaluate_Plus_nn (Literal 0) ae2 e 0 n2 (S_evaluate_Literal 0 e)). Check (S_evaluate_Plus_nn (Literal 0) ae2 e 0 n2 (S_evaluate_Literal 0 e) E_ae2). rewrite <- (Nat.add_0_l n2). exact (S_evaluate_Plus_nn (Literal 0) ae2 e 0 n2 (S_evaluate_Literal 0 e) E_ae2). - destruct S_evaluate as [S_evaluate_Literal [_ [[_ [S_evaluate_Plus_nm _]] _]]]. Check (S_evaluate_Plus_nm (Literal 0) ae2 e). Check (S_evaluate_Plus_nm (Literal 0) ae2 e 0 m2). Check (S_evaluate_Literal 0 e). Check (S_evaluate_Plus_nm (Literal 0) ae2 e 0 m2 (S_evaluate_Literal 0 e)). Check (S_evaluate_Plus_nm (Literal 0) ae2 e 0 m2 (S_evaluate_Literal 0 e) E_ae2). exact (S_evaluate_Plus_nm (Literal 0) ae2 e 0 m2 (S_evaluate_Literal 0 e) E_ae2). Qed. (* ***** *) (* Exercise 07b, with a solution *) Proposition Literal_0_is_neutral_for_Plus_on_the_left_rtl : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_rtl evaluate -> forall (ae2 : arithmetic_expression) (e : environment nat), evaluate (Plus (Literal 0) ae2) e = evaluate ae2 e. Proof. intros evaluate S_evaluate ae2 e. case (evaluate ae2 e) as [n2 | m2] eqn:E_ae2. - destruct S_evaluate as [S_evaluate_Literal [_ [[S_evaluate_Plus_nn [_ _]] _]]]. Check (S_evaluate_Plus_nn (Literal 0) ae2 e n2 0 E_ae2). Check (S_evaluate_Literal 0 e). Check (S_evaluate_Plus_nn (Literal 0) ae2 e n2 0 E_ae2 (S_evaluate_Literal 0 e)). rewrite <- (Nat.add_0_l n2). exact (S_evaluate_Plus_nn (Literal 0) ae2 e n2 0 E_ae2 (S_evaluate_Literal 0 e)). - destruct S_evaluate as [S_evaluate_Literal [_ [[_ [_ S_evaluate_Plus_m]] _]]]. Check (S_evaluate_Plus_m (Literal 0) ae2 e m2 E_ae2). exact (S_evaluate_Plus_m (Literal 0) ae2 e m2 E_ae2). Qed. (* ********** *) (* Exercise 08a *) Proposition Literal_0_is_neutral_for_Plus_on_the_right_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae1 : arithmetic_expression) (e : environment nat), evaluate (Plus ae1 (Literal 0)) e = evaluate ae1 e. Proof. Abort. (* ***** *) (* Exercise 08b *) Proposition Literal_0_is_neutral_for_Plus_on_the_right_rtl : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_rtl evaluate -> forall (ae1 : arithmetic_expression) (e : environment nat), evaluate (Plus ae1 (Literal 0)) e = evaluate ae1 e. Proof. Abort. (* ********** *) (* Exercise 09a *) Proposition Literal_1_is_neutral_for_Times_on_the_left_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae2 : arithmetic_expression) (e : environment nat), evaluate (Times (Literal 1) ae2) e = evaluate ae2 e. Proof. Abort. (* ***** *) (* Exercise 09b *) Proposition Literal_1_is_neutral_for_Times_on_the_left_rtl : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_rtl evaluate -> forall (ae2 : arithmetic_expression) (e : environment nat), evaluate (Times (Literal 1) ae2) e = evaluate ae2 e. Proof. Abort. (* ********** *) (* Exercise 10a *) Proposition Literal_1_is_neutral_for_Times_on_the_right_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae1 : arithmetic_expression) (e : environment nat), evaluate (Times ae1 (Literal 1)) e = evaluate ae1 e. Proof. Abort. (* ***** *) (* Exercise 10b *) Proposition Literal_1_is_neutral_for_Times_on_the_right_rtl : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_rtl evaluate -> forall (ae1 : arithmetic_expression) (e : environment nat), evaluate (Times ae1 (Literal 1)) e = evaluate ae1 e. Proof. Abort. (* ********** *) (* Exercise 11a, with a solution *) Proposition Plus_is_associative_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae1 ae2 ae3 : arithmetic_expression) (e : environment nat), evaluate (Plus ae1 (Plus ae2 ae3)) e = evaluate (Plus (Plus ae1 ae2) ae3) e. Proof. intros evaluate S_evaluate ae1 ae2 ae3 e. case (evaluate ae1 e) as [n1 | m1] eqn:E_ae1. - case (evaluate ae2 e) as [n2 | m2] eqn:E_ae2. + case (evaluate ae3 e) as [n3 | m3] eqn:E_ae3. * destruct S_evaluate as [_ [_ [[S_evaluate_Plus_nn [_ _]] _]]]. Check (S_evaluate_Plus_nn ae1 (Plus ae2 ae3) e). Check (S_evaluate_Plus_nn ae1 (Plus ae2 ae3) e n1). Check (S_evaluate_Plus_nn ae2 ae3 e n2 n3). Check (S_evaluate_Plus_nn ae2 ae3 e n2 n3 E_ae2 E_ae3). Check (S_evaluate_Plus_nn ae1 (Plus ae2 ae3) e n1 (n2 + n3)). Check (S_evaluate_Plus_nn ae1 (Plus ae2 ae3) e n1 (n2 + n3) E_ae1). Check (S_evaluate_Plus_nn ae1 (Plus ae2 ae3) e n1 (n2 + n3) E_ae1 (S_evaluate_Plus_nn ae2 ae3 e n2 n3 E_ae2 E_ae3)). rewrite -> (S_evaluate_Plus_nn ae1 (Plus ae2 ae3) e n1 (n2 + n3) E_ae1 (S_evaluate_Plus_nn ae2 ae3 e n2 n3 E_ae2 E_ae3)). Check (S_evaluate_Plus_nn ae1 ae2 e n1 n2 E_ae1 E_ae2). Check (S_evaluate_Plus_nn (Plus ae1 ae2) ae3 e (n1 + n2) n3 (S_evaluate_Plus_nn ae1 ae2 e n1 n2 E_ae1 E_ae2) E_ae3). rewrite -> (S_evaluate_Plus_nn (Plus ae1 ae2) ae3 e (n1 + n2) n3 (S_evaluate_Plus_nn ae1 ae2 e n1 n2 E_ae1 E_ae2) E_ae3). rewrite -> Nat.add_assoc. reflexivity. * destruct S_evaluate as [_ [_ [[S_evaluate_Plus_nn [S_evaluate_Plus_nm _]] _]]]. Check (S_evaluate_Plus_nm ae1 (Plus ae2 ae3) e n1 m3 E_ae1). (* : evaluate (Plus ae2 ae3) e = Expressible_msg m3 -> evaluate (Plus ae1 (Plus ae2 ae3)) e = Expressible_msg m3 *) Check (S_evaluate_Plus_nm ae2 ae3 e n2 m3 E_ae2 E_ae3). Check (S_evaluate_Plus_nm ae1 (Plus ae2 ae3) e n1 m3 E_ae1 (S_evaluate_Plus_nm ae2 ae3 e n2 m3 E_ae2 E_ae3)). rewrite -> (S_evaluate_Plus_nm ae1 (Plus ae2 ae3) e n1 m3 E_ae1 (S_evaluate_Plus_nm ae2 ae3 e n2 m3 E_ae2 E_ae3)). Check (S_evaluate_Plus_nm (Plus ae1 ae2) ae3 e). Check (S_evaluate_Plus_nm (Plus ae1 ae2) ae3 e (n1 + n2) m3). Check (S_evaluate_Plus_nn ae1 ae2 e n1 n2 E_ae1 E_ae2). Check (S_evaluate_Plus_nm (Plus ae1 ae2) ae3 e (n1 + n2) m3 (S_evaluate_Plus_nn ae1 ae2 e n1 n2 E_ae1 E_ae2)). Check (S_evaluate_Plus_nm (Plus ae1 ae2) ae3 e (n1 + n2) m3 (S_evaluate_Plus_nn ae1 ae2 e n1 n2 E_ae1 E_ae2) E_ae3). rewrite -> (S_evaluate_Plus_nm (Plus ae1 ae2) ae3 e (n1 + n2) m3 (S_evaluate_Plus_nn ae1 ae2 e n1 n2 E_ae1 E_ae2) E_ae3). reflexivity. + destruct S_evaluate as [_ [_ [[S_evaluate_Plus_nn [S_evaluate_Plus_nm S_evaluate_Plus_m]] _]]]. Check (S_evaluate_Plus_nm ae1 (Plus ae2 ae3) e n1 m2). Check (S_evaluate_Plus_nm ae1 (Plus ae2 ae3) e n1 m2 E_ae1). Check (S_evaluate_Plus_m ae2 ae3 e m2 E_ae2). Check (S_evaluate_Plus_nm ae1 (Plus ae2 ae3) e n1 m2 E_ae1 (S_evaluate_Plus_m ae2 ae3 e m2 E_ae2)). rewrite -> (S_evaluate_Plus_nm ae1 (Plus ae2 ae3) e n1 m2 E_ae1 (S_evaluate_Plus_m ae2 ae3 e m2 E_ae2)). Check (S_evaluate_Plus_nm ae1 ae2 e n1 m2 E_ae1 E_ae2). Check (S_evaluate_Plus_m (Plus ae1 ae2) ae3 e m2). Check (S_evaluate_Plus_m (Plus ae1 ae2) ae3 e m2 (S_evaluate_Plus_nm ae1 ae2 e n1 m2 E_ae1 E_ae2)). rewrite -> (S_evaluate_Plus_m (Plus ae1 ae2) ae3 e m2 (S_evaluate_Plus_nm ae1 ae2 e n1 m2 E_ae1 E_ae2)). reflexivity. - destruct S_evaluate as [_ [_ [[_ [_ S_evaluate_Plus_m]] _]]]. Check (S_evaluate_Plus_m ae1 (Plus ae2 ae3) e m1 E_ae1). rewrite -> (S_evaluate_Plus_m ae1 (Plus ae2 ae3) e m1 E_ae1). Check (S_evaluate_Plus_m ae1 ae2 e m1 E_ae1). Check (S_evaluate_Plus_m (Plus ae1 ae2) ae3 e m1). Check (S_evaluate_Plus_m (Plus ae1 ae2) ae3 e m1 (S_evaluate_Plus_m ae1 ae2 e m1 E_ae1)). rewrite -> (S_evaluate_Plus_m (Plus ae1 ae2) ae3 e m1 (S_evaluate_Plus_m ae1 ae2 e m1 E_ae1)). reflexivity. Qed. (* ***** *) (* Exercise 11b, with some food for thought *) Proposition Plus_is_associative_rtl : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_rtl evaluate -> forall (ae1 ae2 ae3 : arithmetic_expression) (e : environment nat), evaluate (Plus ae1 (Plus ae2 ae3)) e = evaluate (Plus (Plus ae1 ae2) ae3) e. Proof. intros evaluate S_evaluate ae1 ae2 ae3 e. case (evaluate ae3 e) as [n3 | m3] eqn:E_ae3. - case (evaluate ae2 e) as [n2 | m2] eqn:E_ae2. + case (evaluate ae1 e) as [n1 | m1] eqn:E_ae1. * admit. * admit. + admit. - admit. Restart. intros evaluate S_evaluate ae1 ae2 ae3 e. case (evaluate ae3 e) as [n3 | m3] eqn:E_ae3; case (evaluate ae2 e) as [n2 | m2] eqn:E_ae2; case (evaluate ae1 e) as [n1 | m1] eqn:E_ae1. - admit. - admit. - admit. - admit. - admit. - admit. - admit. - admit. Abort. (* ********** *) (* Exercise 12a *) Proposition Times_is_associative_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae1 ae2 ae3 : arithmetic_expression) (e : environment nat), evaluate (Times ae1 (Times ae2 ae3)) e = evaluate (Times (Times ae1 ae2) ae3) e. Proof. Abort. (* ***** *) (* Exercise 12b *) Proposition Times_is_associative_rtl : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_rtl evaluate -> forall (ae1 ae2 ae3 : arithmetic_expression) (e : environment nat), evaluate (Times ae1 (Times ae2 ae3)) e = evaluate (Times (Times ae1 ae2) ae3) e. Proof. Abort. (* ********** *) (* Exercise 13a, with a solution *) Proposition Literal_0_is_absorbing_for_Times_on_the_left_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae2 : arithmetic_expression) (e : environment nat), evaluate (Times (Literal 0) ae2) e = evaluate (Literal 0) e. Proof. intros evaluate S_evaluate ae2 e. case (evaluate ae2 e) as [n2 | m2] eqn:E_ae2. - destruct S_evaluate as [S_evaluate_Literal [_ [_ [S_evaluate_Times_nn [_ _]]]]]. Check (S_evaluate_Times_nn (Literal 0) ae2 e 0 n2 (S_evaluate_Literal 0 e) E_ae2). rewrite -> (S_evaluate_Times_nn (Literal 0) ae2 e 0 n2 (S_evaluate_Literal 0 e) E_ae2). rewrite -> Nat.mul_0_l. rewrite -> (S_evaluate_Literal 0 e). reflexivity. - destruct S_evaluate as [S_evaluate_Literal [_ [_ [_ [S_evaluate_Times_nm _]]]]]. Check (S_evaluate_Times_nm (Literal 0) ae2 e 0 m2 (S_evaluate_Literal 0 e) E_ae2). rewrite -> (S_evaluate_Times_nm (Literal 0) ae2 e 0 m2 (S_evaluate_Literal 0 e) E_ae2). rewrite -> (S_evaluate_Literal 0 e). Abort. Theorem Literal_0_is_not_absorbing_for_Times_on_the_left_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> exists (ae2 : arithmetic_expression) (e : environment nat), evaluate (Times (Literal 0) ae2) e <> evaluate (Literal 0) e. Proof. intros evaluate S_evaluate. exists (Name "x"%string). exists (mt nat). destruct S_evaluate as [S_evaluate_Literal [S_evaluate_Name [_ [_ [S_evaluate_Times_nm _]]]]]. Check (S_evaluate_Times_nm (Literal 0) (Name "x"%string) (mt nat) 0 (Undeclared_name "x"%string) (S_evaluate_Literal 0 (mt nat)) (S_evaluate_Name "x"%string (mt nat))). rewrite -> (S_evaluate_Times_nm (Literal 0) (Name "x"%string) (mt nat) 0 (Undeclared_name "x"%string) (S_evaluate_Literal 0 (mt nat)) (S_evaluate_Name "x"%string (mt nat))). rewrite -> (S_evaluate_Literal 0 (mt nat)). unfold not. intro H_absurd; discriminate H_absurd. Qed. (* ***** *) (* Exercise 13b *) Proposition Literal_0_is_absorbing_for_Times_on_the_right_rtl : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_rtl evaluate -> forall (ae2 : arithmetic_expression) (e : environment nat), evaluate (Times (Literal 0) ae2) e = evaluate (Literal 0) e. Proof. Abort. (* ********** *) (* Exercise 14a *) Proposition Literal_0_is_absorbing_for_Times_on_the_right_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae1 : arithmetic_expression) (e : environment nat), evaluate (Times ae1 (Literal 0)) e = evaluate (Literal 0) e. Proof. Abort. (* ***** *) (* Exercise 14b *) Proposition Literal_0_is_absorbing_for_Times_on_the_right_rtl : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_rtl evaluate -> forall (ae1 : arithmetic_expression) (e : environment nat), evaluate (Times ae1 (Literal 0)) e = evaluate (Literal 0) e. Proof. Abort. (* ********** *) (* Exercise 15a *) Proposition Plus_is_commutative_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae1 ae2 : arithmetic_expression) (e : environment nat), evaluate (Plus ae1 ae2) e = evaluate (Plus ae2 ae1) e. Proof. Abort. (* ***** *) (* Exercise 15b *) Proposition Plus_is_commutative_rtl : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_rtl evaluate -> forall (ae1 ae2 : arithmetic_expression) (e : environment nat), evaluate (Plus ae1 ae2) e = evaluate (Plus ae2 ae1) e. Proof. Abort. (* ********** *) (* Exercise 16a *) Proposition Times_is_commutative_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae1 ae2 : arithmetic_expression) (e : environment nat), evaluate (Times ae1 ae2) e = evaluate (Times ae2 ae1) e. Proof. Abort. (* ***** *) (* Exercise 16b *) Proposition Times_is_commutative_rtl : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_rtl evaluate -> forall (ae1 ae2 : arithmetic_expression) (e : environment nat), evaluate (Times ae1 ae2) e = evaluate (Times ae2 ae1) e. Proof. Abort. (* ********** *) (* Exercise 17a *) Proposition Times_distributes_over_Plus_on_the_left_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae1 ae2 ae3 : arithmetic_expression) (e : environment nat), evaluate (Times ae1 (Plus ae2 ae3)) e = evaluate (Plus (Times ae1 ae2) (Times ae1 ae3)) e. Proof. Abort. (* ***** *) (* Exercise 17b *) Proposition Times_distributes_over_Plus_on_the_left_rtl : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_rtl evaluate -> forall (ae1 ae2 ae3 : arithmetic_expression) (e : environment nat), evaluate (Times ae1 (Plus ae2 ae3)) e = evaluate (Plus (Times ae1 ae2) (Times ae1 ae3)) e. Proof. Abort. (* ********** *) (* Exercise 18a *) Proposition Times_distributes_over_Plus_on_the_right_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae1 ae2 ae3 : arithmetic_expression) (e : environment nat), evaluate (Times (Plus ae1 ae2) ae3) e = evaluate (Plus (Times ae1 ae3) (Times ae2 ae3)) e. Proof. Abort. (* ***** *) (* Exercise 18b *) Proposition Times_distributes_over_Plus_on_the_right_rtl : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_rtl evaluate -> forall (ae1 ae2 ae3 : arithmetic_expression) (e : environment nat), evaluate (Times (Plus ae1 ae2) ae3) e = evaluate (Plus (Times ae1 ae3) (Times ae2 ae3)) e. Proof. Abort. (* ********** *) (* Exercise 19 *) (* ***** *) (* The vacuous example from the lecture notes: *) Proposition sufficient_conditions_for_Literal_0_to_be_neutral_for_Plus_on_the_left_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae : arithmetic_expression) (e : environment nat), True -> evaluate (Plus (Literal 0) ae) e = evaluate ae e. Proof. intros evaluate S_evaluate_Literal ae e _. revert evaluate S_evaluate_Literal ae e. exact Literal_0_is_neutral_for_Plus_on_the_left_ltr. Qed. Proposition necessary_conditions_for_Literal_0_to_be_neutral_for_Plus_on_the_left_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae : arithmetic_expression) (e : environment nat), evaluate (Plus (Literal 0) ae) e = evaluate ae e -> True. Proof. intros _ _ _ _ _. Check I. exact I. Qed. Proposition Literal_0_is_conditionally_neutral_for_Plus_on_the_left_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae : arithmetic_expression) (e : environment nat), True <-> evaluate (Plus (Literal 0) ae) e = evaluate ae e. Proof. intros evaluate S_evaluate_Literal ae e. split; revert evaluate S_evaluate_Literal ae e. - exact sufficient_conditions_for_Literal_0_to_be_neutral_for_Plus_on_the_left_ltr. - exact necessary_conditions_for_Literal_0_to_be_neutral_for_Plus_on_the_left_ltr. Qed. (* ***** *) (* Actual example from Exercise 13a: *) Proposition sufficient_condition_for_Literal_0_to_be_absorbing_for_Times_on_the_left_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae2 : arithmetic_expression) (e : environment nat), (exists n2 : nat, evaluate ae2 e = Expressible_nat n2) -> evaluate (Times (Literal 0) ae2) e = evaluate (Literal 0) e. Proof. intros evaluate S_evaluate ae2 e [n2 E_ae2]. destruct S_evaluate as [S_evaluate_Literal [_ [_ [S_evaluate_Times_nn [_ _]]]]]. Check (S_evaluate_Times_nn (Literal 0) ae2 e 0 n2 (S_evaluate_Literal 0 e) E_ae2). rewrite -> (S_evaluate_Times_nn (Literal 0) ae2 e 0 n2 (S_evaluate_Literal 0 e) E_ae2). rewrite -> Nat.mul_0_l. rewrite -> (S_evaluate_Literal 0 e). reflexivity. Qed. Proposition necessary_condition_for_Literal_0_to_be_absorbing_for_Times_on_the_left_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae2 : arithmetic_expression) (e : environment nat), evaluate (Times (Literal 0) ae2) e = evaluate (Literal 0) e -> exists n2 : nat, evaluate ae2 e = Expressible_nat n2. Proof. intros evaluate S_evaluate ae2 e H_ae2. case (evaluate ae2 e) as [n2 | m2] eqn:E_ae2. - exists n2. reflexivity. - destruct S_evaluate as [S_evaluate_Literal [_ [_ [_ [S_evaluate_Times_nm _]]]]]. Check (S_evaluate_Times_nm (Literal 0) ae2 e 0 m2 (S_evaluate_Literal 0 e) E_ae2). rewrite -> (S_evaluate_Times_nm (Literal 0) ae2 e 0 m2 (S_evaluate_Literal 0 e) E_ae2) in H_ae2. rewrite -> (S_evaluate_Literal 0 e) in H_ae2. discriminate H_ae2. Qed. Proposition Literal_0_is_conditionally_absorbing_for_Times_on_the_left_ltr : forall evaluate : arithmetic_expression -> environment nat -> expressible_value, specification_of_evaluate_ltr evaluate -> forall (ae2 : arithmetic_expression) (e : environment nat), (exists n2 : nat, evaluate ae2 e = Expressible_nat n2) <-> evaluate (Times (Literal 0) ae2) e = evaluate (Literal 0) e. Proof. intros evaluate S_evaluate ae2 e. split; revert evaluate S_evaluate ae2 e. - exact sufficient_condition_for_Literal_0_to_be_absorbing_for_Times_on_the_left_ltr. - exact necessary_condition_for_Literal_0_to_be_absorbing_for_Times_on_the_left_ltr. Qed. (* ********** *) (* end of week-12_observational-equivalence.v *)