(* ***************************************************************** *)
(* *)
(* Released: 2021/03/17. *)
(* Due: 2021/03/21, 23:59:59, CST. *)
(* *)
(* 0. Read instructions carefully before start writing your answer. *)
(* *)
(* 1. You should not add any hypotheses in this assignment. *)
(* Necessary ones have been provided for you. *)
(* *)
(* 2. In order to check whether you have finished all tasks or not, *)
(* just see whether all "Admitted" has been replaced. *)
(* *)
(* 3. You should submit this file (Assignment3a.v) on CANVAS. *)
(* *)
(* 4. Only valid Coq files are accepted. In other words, please *)
(* make sure that your file does not generate a Coq error. A *)
(* way to check that is: click "compile buffer" for this file *)
(* and see whether an "Assignment3a.vo" file is generated. *)
(* *)
(* 5. Do not copy and paste others' answer. *)
(* *)
(* 6. Using any theorems and/or tactics provided by Coq's standard *)
(* library is allowed in this assignment, if not specified. *)
(* *)
(* 7. When you finish, answer the following question: *)
(* *)
(* Who did you discuss with when finishing this *)
(* assignment? Your answer to this question will *)
(* NOT affect your grade. *)
(* (* FILL IN YOUR ANSWER HERE AS COMMENT *) *)
(* *)
(* ***************************************************************** *)
Require Import PL.Imp.
Require Import Coq.micromega.Psatz.
Require Import Coq.Lists.List. Import ListNotations.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
(* ################################################################# *)
(** * Task 1: Understanding Denotations *)
(** In this task, you will read descriptions about program states and decide
whether the following pairs of programs states belong to corresponding
programs' denotations. *)
(** **** Exercise: 1 star, standard *)
Module Task1_1.
(** Suppose [X] and [Y] are different program variables. If [st X = 1] and
[st Y = 2], then does (st, st) belong to the following program's denotation?
Y ::= X + 1
1: Yes. 2: No. *)
Definition my_choice: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
End Task1_1.
(** [] *)
(** **** Exercise: 1 star, standard *)
Module Task1_2.
(** Suppose [X] is a program variables. If [st1 X = 100], [st2 X = 1] and all
other variables in [st1] and [st2] are zero, then does (st1, st2) belong to
the following program's denotation?
While 1 <= X Do X ::= X + 1 EndWhile
1: Yes. 2: No. *)
Definition my_choice: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
End Task1_2.
(** [] *)
(** **** Exercise: 1 star, standard *)
Module Task1_3.
(** Suppose [X] and [Y] are different program variables. If [st1 X = 1],
[st1 Y = 2], [st2 X = 2], [st2 Y = 1] and all other variables in [st1] and
[st2] are zero, then does (st1, st2) belong to the following program's
denotation?
Z ::= X;; X ::= Y;; Y ::= Z
1: Yes. 2: No. *)
Definition my_choice: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
End Task1_3.
(** [] *)
(* ################################################################# *)
(** * Task 2: Understanding Higher-Order Functions *)
(** Suppose [f] and [g] are both functions from [A] to [A]. How shall we define
the function that applies [f] first and then applies [g]? *)
(** **** Exercise: 2 stars, standard (compose) *)
Definition compose {A: Type} (f g: A -> A): A -> A
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** It is obvious that [ compose f (compose g h) ] is equivalent with
[ compose (compose f g) h ]. Your task is to prove it in Coq. *)
Theorem compose_assoc: forall f g h: Z -> Z,
Func.equiv (compose f (compose g h)) (compose (compose f g) h).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(* ################################################################# *)
(** * Task 3: Recursive Reasoning About Expressions, A Transformation *)
(** We know that for any integer expressions [a1], [a2] and [a3],
[[ a1 + (a2 + a3) and (a1 + a2) + a3 ]]
[[ a1 * (a2 * a3) and (a1 * a2) * a3 ]]
are equivalent expressions. In other words, [APlus] and [AMult] are
associative in the sense of expressions equivalence. Also, if [AMinus] is
taken into consideration,
[[ a1 - (a2 + a3) and (a1 - a2) - a3 ]]
[[ a1 - (a2 - a3) and (a1 - a2) + a3 ]]
[[ a1 + (a2 - a3) and (a1 + a2) - a3 ]]
are also equivalent expressions. Here are their Coq statements. *)
(** **** Exercise: 1 star, standard (APlus_assoc) *)
Lemma APlus_assoc: forall a1 a2 a3,
aexp_equiv (a1 + (a2 + a3)) ((a1 + a2) + a3).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 1 star, standard (APlus_AMinus_assoc) *)
Lemma APlus_AMinus_assoc: forall a1 a2 a3,
aexp_equiv (a1 + (a2 - a3)) ((a1 + a2) - a3).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 1 star, standard (AMinus_APlus_assoc) *)
Lemma AMinus_APlus_assoc: forall a1 a2 a3,
aexp_equiv (a1 - (a2 + a3)) ((a1 - a2) - a3).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 1 star, standard (AMinus_AMinus_assoc) *)
Lemma AMinus_AMinus_assoc: forall a1 a2 a3,
aexp_equiv (a1 - (a2 - a3)) ((a1 - a2) + a3).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
Lemma AMult_assoc: forall a1 a2 a3,
aexp_equiv (a1 * (a2 * a3)) ((a1 * a2) * a3).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(* Due to this consideration, we can always transform an expression to a
''left-associative'' one. We define this transformation as follows.
The first three are auxiliary definitions. *)
Fixpoint APlus_left_assoc (a0 a: aexp): aexp :=
(* Suppose [a0] and [a] are both ''left-associative'', define the
transformation result of [a0 + a] *)
match a with
| APlus a1 a2 => APlus (APlus_left_assoc a0 a1) a2
| AMinus a1 a2 => AMinus (APlus_left_assoc a0 a1) a2
| _ => APlus a0 a
end.
Fixpoint AMinus_left_assoc (a0 a: aexp): aexp :=
(* Suppose [a0] and [a] are both ''left-associative'', define the
transformation result of [a0 - a] *)
match a with
| APlus a1 a2 => AMinus (AMinus_left_assoc a0 a1) a2
| AMinus a1 a2 => APlus (AMinus_left_assoc a0 a1) a2
| _ => AMinus a0 a
end.
Fixpoint AMult_left_assoc (a0 a: aexp): aexp :=
(* Suppose [a0] and [a] are both ''left-associative'', define the
transformation result of [a0 * a] *)
match a with
| AMult a1 a2 => AMult (AMult_left_assoc a0 a1) a2
| _ => AMult a0 a
end.
(** Then, [left_assoc] is our final definition. *)
Fixpoint left_assoc (a: aexp): aexp :=
match a with
| ANum n => ANum n
| AId X => AId X
| APlus a1 a2 => APlus_left_assoc (left_assoc a1) (left_assoc a2)
| AMinus a1 a2 => AMinus_left_assoc (left_assoc a1) (left_assoc a2)
| AMult a1 a2 => AMult_left_assoc (left_assoc a1) (left_assoc a2)
end.
(** Now, your task is to prove it sound, i.e. the expression after [left_assoc]
transformation is equivalent to the original one. We first prove three
auxiliary functions's soundness. *)
(** **** Exercise: 2 stars, standard (APlus_left_assoc_sound) *)
Lemma APlus_left_assoc_sound: forall a0 a,
aexp_equiv (APlus_left_assoc a0 a) (APlus a0 a).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard (AMinus_left_assoc_sound) *)
Lemma AMinus_left_assoc_sound: forall a0 a,
aexp_equiv (AMinus_left_assoc a0 a) (AMinus a0 a).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard (AMult_left_assoc_sound) *)
Lemma AMult_left_assoc_sound: forall a0 a,
aexp_equiv (AMult_left_assoc a0 a) (AMult a0 a).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** Now, you are ready to prove our main theorem. *)
(** **** Exercise: 2 stars, standard (left_assoc_sound) *)
Theorem left_assoc_sound: forall a,
aexp_equiv (left_assoc a) a.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** Besides soundness, it is critical that results of [left_assoc] are actually
in a ''left-associative'' form. We first define [partially_right_assoc], the
negation of ''left-associative'', that is, at least one subexpression is
right associative. Described as follows, its definition contains two _match_
expressions. The first one says: [a]'s top level syntax tree is right
associative. The second one says: [a]'s subexpressions has at least one
right associative subexpression inside. *)
Fixpoint partially_right_assoc (a: aexp): Prop :=
match a with
| APlus _ (APlus _ _) => True
| APlus _ (AMinus _ _) => True
| AMinus _ (APlus _ _) => True
| AMinus _ (AMinus _ _) => True
| AMult _ (AMult _ _) => True
| _ => False
end \/
match a with
| APlus a1 a2 => partially_right_assoc a1 \/ partially_right_assoc a2
| AMinus a1 a2 => partially_right_assoc a1 \/ partially_right_assoc a2
| AMult a1 a2 => partially_right_assoc a1 \/ partially_right_assoc a2
| _ => False
end.
(** Then we define [fully_left_associative]. *)
Definition fully_left_associative (a: aexp): Prop :=
~ partially_right_assoc a.
(** Similar to your soundness proof above, you need to prove three lemmas about
auxiliary funcstions and [fully_left_associative] first. Hint: remember that
you can use [tauto] solve propositional logic proof goals automatically. *)
(** **** Exercise: 2 stars, standard (APlus_left_assoc_fully_left_associative) *)
Lemma APlus_left_assoc_fully_left_associative: forall a0 a,
fully_left_associative a0 ->
fully_left_associative a ->
fully_left_associative (APlus_left_assoc a0 a).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard (AMinus_left_assoc_fully_left_associative) *)
Lemma AMinus_left_assoc_fully_left_associative: forall a0 a,
fully_left_associative a0 ->
fully_left_associative a ->
fully_left_associative (AMinus_left_assoc a0 a).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard (AMult_left_assoc_fully_left_associative) *)
Lemma AMult_left_assoc_fully_left_associative: forall a0 a,
fully_left_associative a0 ->
fully_left_associative a ->
fully_left_associative (AMult_left_assoc a0 a).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** Lastly, please prove that results of [left_assoc] always satisfy
[fully_left_associative]. *)
(** **** Exercise: 2 stars, standard (left_assoc_fully_left_associative) *)
Lemma left_assoc_fully_left_associative: forall a,
fully_left_associative (left_assoc a).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** You may wonder whether [left_assoc] is a meaningful operation. Well, it
might be. Try to answer the following questions about it. *)
(** **** Exercise: 1 star, standard *)
(** In comparison, which one of the following is the better optimazation?
- do [fold_constants] directly;
- do [fold_constants] after [left_assoc].
Choose one correct statement:
0. They always generate results with the same length.
1. The first one always generates shorter (or equivalent) result and
statement 0 is wrong.
2. The second one always generates shorter (or equivalent) result and
statement 0 is wrong.
3. They are not comparable. *)
Definition my_choice_1: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(** **** Exercise: 1 star, standard *)
(** In comparison, which one of the following is the better optimazation?
- do [fold_constants] directly;
- do [fold_constants], then [left_assoc], and [fold_constants] again
in the end
Choose one correct statement:
0. They always generate results with the same length.
1. The first one always generates shorter (or equivalent) result and
statement 0 is wrong.
2. The second one always generates shorter (or equivalent) result and
statement 0 is wrong.
3. They are not comparable. *)
Definition my_choice_2: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(* ################################################################# *)
(** * Task 4: Equivalence and Congruence *)
(** In lectures, we defined a [same_structure] relation for binary trees. *)
Inductive tree: Type :=
| Leaf: tree
| Node (l: tree) (v: Z) (r: tree): tree.
Fixpoint same_structure (t1 t2: tree): Prop :=
match t1, t2 with
| Leaf, Leaf => True
| Leaf, Node _ _ _ => False
| Node _ _ _, Leaf => False
| Node l1 _ r1, Node l2 _ r2 => same_structure l1 l2 /\ same_structure r1 r2
end.
(** Now, your task is prove that it is a equivalence relation and a congruence
w.r.t. tree construction [Node] and tree reverse operation. *)
(** **** Exercise: 1 star, standard (same_structure_refl) *)
Lemma same_structure_refl: Reflexive same_structure.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard (same_structure_sym) *)
Lemma same_structure_sym: Symmetric same_structure.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard (same_structure_trans) *)
Lemma same_structure_trans: Transitive same_structure.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 1 star, standard (same_structure_Node_congr) *)
Lemma same_structure_Node_congr:
Proper (same_structure ==> eq ==> same_structure ==> same_structure) Node.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
Fixpoint tree_reverse (t: tree): tree :=
match t with
| Leaf => Leaf
| Node l v r => Node (tree_reverse r) v (tree_reverse l)
end.
(** **** Exercise: 2 stars, standard (same_structure_tree_reverse_congr) *)
Lemma same_structure_tree_reverse_congr:
Proper (same_structure ==> same_structure) tree_reverse.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(* 2021-03-17 12:19 *)