(* ***************************************************************** *)
(* *)
(* Released: 2021/03/22. *)
(* Due: 2021/03/26, 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 (Assignment3b.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 "Assignment3b.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 5: Understanding Bourbaki-Witt Fix Points *)
Module Task5_1.
(** Let [A] be the set of all subsets of integers and let [<=] be the inclusion
relation. In other words, for any [a b: A], [a <= b] if and only if [a] is
a subset of [b]. Obviously, [<=] is a partial order on [A], and moreover, it
is a complete partial ordering on [A].
Consider the following function [f] from [A] to [A] and answer questions.
- Given [X: A], an integer [u] is an element of [ f(X) ] if and only if [-u]
is an element of [X]. *)
(** **** Exercise: 1 star, standard *)
(** Is this function [f] a monotonic function w.r.t. the partial order [<=] on
[A]? 1: Yes. 2: No. *)
Definition my_answer_1: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(** **** Exercise: 1 star, standard *)
(** Is this function [f] a continuous function w.r.t. the CPO [<=]? 1: Yes.
2: No. *)
Definition my_answer_2: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(** **** Exercise: 1 star, standard *)
(** How many fixpoints does [f] have? 1: Zero. 2: Exactly one. 3: Finite but
more than one. 4: Infinite. *)
Definition my_answer_3: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(** **** Exercise: 1 star, standard *)
(** Is the following statement correct? 1: Yes. 2: No.
The function [f] has at least one fixpoint and the singleton set [ {0} ] is
its least fixpoint w.r.t. the order [<=]. *)
Definition my_answer_4: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
End Task5_1.
Module Task5_2.
(** Let [A] and [<=] be the same set and CPO described in the last sub-task.
Consider the following function [f] from [A] to [A] and answer questions.
- Given [X: A], an integer [u] is an element of [ f(X) ] if and only if
[u = 0] or [u - 1] is an element of [X]. *)
(** **** Exercise: 1 star, standard *)
(** Is this function [f] a monotonic function w.r.t. the partial order [<=] on
[A]? 1: Yes. 2: No. *)
Definition my_answer_1: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(** **** Exercise: 1 star, standard *)
(** Is this function [f] a continuous function w.r.t. the CPO [<=]? 1: Yes.
2: No. *)
Definition my_answer_2: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(** **** Exercise: 1 star, standard *)
(** Which is the least fixpoint of [f] w.r.t. [<=]?
1: The empty set.
2: The set of all integers.
3: The set of all non-negative integers.
4: The singleton set with integer zero.
5: None of the above. *)
Definition my_answer_3: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(** Which is the greatest fixpoint of [f] w.r.t. [<=]?
1: The empty set.
2: The set of all integers.
3: The set of all non-negative integers.
4: The singleton set with integer zero.
5: None of the above. *)
Definition my_answer_4: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
End Task5_2.
Module Task5_3.
(** Let [A] and [<=] be the same set and CPO described in the last sub-task.
Consider the following function [f] from [A] to [A] and answer questions.
Given [X: A],
- [0] is an element of [ f(X) ] if all positive integers are elements of [X]
- [1] is an element of [ f(X) ]
- a integer [u], other than zero and one, is an element of [ f(X) ] if
[u - 1] is an element of [X]. *)
(** **** Exercise: 1 star, standard *)
(** Is this function [f] a monotonic function w.r.t. the partial order [<=] on
[A]? 1: Yes. 2: No. *)
Definition my_answer_1: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(** **** Exercise: 1 star, standard *)
(** Is this function [f] a continuous function w.r.t. the CPO [<=]? 1: Yes.
2: No. *)
Definition my_answer_2: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(** **** Exercise: 1 star, standard *)
(** Which is the least fixpoint of [f] w.r.t. [<=]?
1: The empty set.
2: The set of all integers.
3: The set of all positive integers.
4: The singleton set with integer zero.
5: None of the above. *)
Definition my_answer_3: Z
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
End Task5_3.
(* ################################################################# *)
(** * Task 6: Understanding Loops' Denotational Semantics *)
Section BW_FixPoint.
(** Given a boolean expression [b] and a loop body's denotation [d], we have
defined [loop_sem b d] as the whole loop's denotation in lectures. We also
know that [loop_sem b d] is the least fix point of the following function
[F], although its construction is not identical to the one in Bourbaki-Witt
Fix Point theorem. *)
Variable b: bexp.
Variable d: state -> state -> Prop.
Definition F X := if_sem b (BinRel.concat d X) BinRel.id.
(** In other words, [loop_sem b d] is equivalent with [F (loop_sem b d)]. *)
(** Now, let's discover the relation between our definition of [loop_sem] and
Bourbaki-Witt's construction. Bourbaki-Witt's construction is based on a
bottom element, in this case, the empty relation. *)
Definition Bot: state -> state -> Prop := BinRel.empty.
(** And the least fix point is the least upper bound of:
- Bot
- F Bot
- F (F Bot)
- F (F (F Bot))
- ... *)
Fixpoint FBot (n: nat) :=
match n with
| O => Bot
| S n' => F (FBot n')
end.
Definition loop_sem' := BinRel.omega_union (FBot).
(** In this case, the least upper bound of a ternary relation sequence is their
[omega_union_sem]. Thus, Bourbaki-Witt's fixpoint can be formalized as
[loop_sem'] above. *)
End BW_FixPoint.
(** Now, let's discover the relationship between [loop_sem]'s construction and
[loop_sem']'s construction.
Hint 1: Both [iter_loop_body] and [FBot] are recursively defined. You may
write [simpl] to use their definitions.
Hint 2: Proving some extra properties about [Bot], [BinRel.union] and
[BinRel.concat] could make your proofs more concise. For example:
[[
forall d: state -> state -> Prop,
BinRel.equiv (BinRel.union Bot d) d
forall d: state -> state -> Prop,
BinRel.equiv (BinRel.union d Bot) d
forall d: state -> state -> Prop,
BinRel.equiv (BinRel.concat d Bot) Bot.
forall d: state -> state -> Prop,
BinRel.equiv (BinRel.concat Bot d) Bot.
forall d: state -> state -> Prop,
BinRel.equiv (BinRel.concat d BinRel.id) d.
forall d: state -> state -> Prop,
BinRel.equiv (BinRel.concat BinRel.id d) d.
]]
*)
(** **** Exercise: 2 stars, standard (FBot1_fact) *)
Fact FBot1_fact: forall b d, BinRel.equiv (iter_loop_body b d 0) (FBot b d 1).
Proof.
intros.
simpl.
unfold F, if_sem.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard (FBot2_fact) *)
Fact FBot2_fact: forall b d,
BinRel.equiv
(BinRel.union (iter_loop_body b d 1) (iter_loop_body b d 0))
(FBot b d 2).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard (FBot_n_fact_statement) *)
(** For generic natural number [n], what is the connection between [FBot b d n]
and [iter_loop_body]? Write down a proposition to describe this connection.
Note that your [FBot_n_fact_statement] should have the following form:
- forall b d n, BinRel.equiv (...) (FBot b d n).
And you probably need to write some auxiliary definition(s) first. *)
Definition FBot_n_fact_statement: Prop
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
(** [] *)
(* 2021-03-22 18:13 *)