(* 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 *) 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. Abort. (* ***** *) (* Exercise 07b *) 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. Abort. (* ********** *) (* 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 *) 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. Abort. (* ***** *) (* Exercise 11b *) 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. 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 *) 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. Abort. (* ***** *) (* 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. (* ********** *) (* Exercise 20 *) Definition specification_of_evaluate_mixed (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) (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)). (* ********** *) (* end of week-12_observational-equivalence.v *)