feat: 3234 current midterms progress
This commit is contained in:
parent
9162dcb311
commit
ff946d3a1c
1773
cs3234/labs/midterm_project.v
Normal file
1773
cs3234/labs/midterm_project.v
Normal file
File diff suppressed because it is too large
Load Diff
754
cs3234/labs/week-05_mystery-functions.v
Normal file
754
cs3234/labs/week-05_mystery-functions.v
Normal file
@ -0,0 +1,754 @@
|
||||
(* week-05_mystery-functions.v *)
|
||||
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
|
||||
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
|
||||
(* Version of 16 Feb 2024 *)
|
||||
|
||||
(* ********** *)
|
||||
|
||||
(* Paraphernalia: *)
|
||||
|
||||
Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
|
||||
|
||||
Require Import Bool Arith.
|
||||
|
||||
Check Nat.eqb.
|
||||
Check (fun i j => Nat.eqb i j).
|
||||
(* so "X =? Y" is syntactic sugar for "Nat.eqb X Y" *)
|
||||
|
||||
Check Bool.eqb.
|
||||
Check (fun b1 b2 => Bool.eqb b1 b2).
|
||||
(* so eqb stands for Bool.eqb *)
|
||||
|
||||
(* ********** *)
|
||||
|
||||
|
||||
Definition specification_of_mystery_function_00 (mf : nat -> nat) :=
|
||||
mf 0 = 1
|
||||
/\
|
||||
forall i j : nat, mf (S (i + j)) = mf i + mf j.
|
||||
|
||||
(* ***** *)
|
||||
|
||||
Proposition there_is_at_most_one_mystery_function_00 :
|
||||
forall f g : nat -> nat,
|
||||
specification_of_mystery_function_00 f ->
|
||||
specification_of_mystery_function_00 g ->
|
||||
forall n : nat,
|
||||
f n = g n.
|
||||
Proof.
|
||||
intros f g.
|
||||
intros [H_f_O H_f_S] [H_g_O H_g_S].
|
||||
intro n.
|
||||
induction n as [| n' IHn'].
|
||||
- rewrite -> H_f_O.
|
||||
symmetry.
|
||||
exact H_g_O.
|
||||
- rewrite <- (Nat.add_0_l n').
|
||||
rewrite -> (H_f_S 0 n').
|
||||
rewrite -> (H_f_O).
|
||||
rewrite -> (H_g_S 0 n').
|
||||
rewrite -> (H_g_O).
|
||||
rewrite -> IHn'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ***** *)
|
||||
|
||||
Definition unit_test_for_mystery_function_00a (mf : nat -> nat) :=
|
||||
(mf 0 =? 1)
|
||||
&&
|
||||
(mf 1 =? 2)
|
||||
&&
|
||||
(mf 2 =? 3)
|
||||
&&
|
||||
(mf 3 =? 4).
|
||||
|
||||
(* etc. *)
|
||||
|
||||
Definition unit_test_for_mystery_function_00b (mf : nat -> nat) :=
|
||||
(mf 0 =? 1) && (mf 1 =? 2) (* etc. *).
|
||||
|
||||
Definition unit_test_for_mystery_function_00c (mf : nat -> nat) :=
|
||||
(mf 0 =? 1) && (mf 1 =? 2) && (mf 2 =? 3) (* etc. *).
|
||||
|
||||
Definition unit_test_for_mystery_function_00d (mf : nat -> nat) :=
|
||||
(mf 0 =? 1) && (mf 1 =? 2) && (mf 2 =? 3) && (mf 3 =? 4)
|
||||
(* etc. *).
|
||||
|
||||
(* ***** *)
|
||||
|
||||
Compute (unit_test_for_mystery_function_00d).
|
||||
|
||||
Definition mystery_function_00 := S.
|
||||
|
||||
Definition less_succinct_mystery_function_00 (n : nat) : nat :=
|
||||
S n.
|
||||
|
||||
Compute (unit_test_for_mystery_function_00d mystery_function_00).
|
||||
|
||||
Theorem there_is_at_least_one_mystery_function_00 :
|
||||
specification_of_mystery_function_00 mystery_function_00.
|
||||
Proof.
|
||||
unfold specification_of_mystery_function_00, mystery_function_00.
|
||||
split.
|
||||
- reflexivity.
|
||||
- intros i j.
|
||||
rewrite -> (plus_Sn_m i (S j)).
|
||||
rewrite <- (plus_n_Sm i j).
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ***** *)
|
||||
|
||||
Definition mystery_function_00_alt := fun (n : nat) => n + 1.
|
||||
|
||||
Theorem there_is_at_least_one_mystery_function_00_alt :
|
||||
specification_of_mystery_function_00 mystery_function_00_alt.
|
||||
Proof.
|
||||
Abort.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
(* Thanks to calvin's eureka lemma *)
|
||||
Definition specification_of_mystery_function_11 (mf : nat -> nat) :=
|
||||
mf 1 = 1
|
||||
/\
|
||||
forall i j : nat,
|
||||
mf (i + j) = mf i + 2 * i * j + mf j.
|
||||
|
||||
Proposition about_mystery_function_11 :
|
||||
forall f : nat -> nat,
|
||||
specification_of_mystery_function_11 f ->
|
||||
f 0 = 0.
|
||||
Proof.
|
||||
intros f.
|
||||
intros [S_f_1 S_f_ij].
|
||||
assert (S_f_0 := (S_f_ij 0 0)).
|
||||
rewrite -> (Nat.add_0_l 0) in S_f_0.
|
||||
rewrite -> (Nat.mul_0_r 2) in S_f_0.
|
||||
rewrite -> (Nat.mul_0_r 0) in S_f_0.
|
||||
rewrite -> (Nat.add_0_r (f 0)) in S_f_0.
|
||||
rewrite <- (Nat.add_0_r (f 0)) in S_f_0 at 1.
|
||||
symmetry.
|
||||
Check Plus.plus_reg_l_stt.
|
||||
Check (Plus.plus_reg_l_stt 0 (f 0) (f 0) S_f_0).
|
||||
exact (Plus.plus_reg_l_stt 0 (f 0) (f 0) S_f_0).
|
||||
Qed.
|
||||
|
||||
Proposition there_is_at_most_one_mystery_function_11 :
|
||||
forall f g : nat -> nat,
|
||||
specification_of_mystery_function_11 f ->
|
||||
specification_of_mystery_function_11 g ->
|
||||
forall n : nat,
|
||||
f n = g n.
|
||||
Proof.
|
||||
intros f g.
|
||||
intros S_f S_g.
|
||||
assert (S_tmp_f := S_f).
|
||||
assert (S_tmp_g := S_g).
|
||||
destruct S_tmp_f as [S_f_1 S_f_ij].
|
||||
destruct S_tmp_g as [S_g_1 S_g_ij].
|
||||
intro x.
|
||||
induction x as [| x' IHx'].
|
||||
- rewrite -> (about_mystery_function_11 g S_g).
|
||||
exact (about_mystery_function_11 f S_f).
|
||||
- rewrite <- (Nat.add_1_l x').
|
||||
rewrite -> (S_f_ij 1 x').
|
||||
rewrite -> S_f_1.
|
||||
rewrite -> IHx'.
|
||||
rewrite -> (S_g_ij 1 x').
|
||||
rewrite -> S_g_1.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_04 (mf : nat -> nat) :=
|
||||
mf 0 = 0
|
||||
/\
|
||||
forall n' : nat,
|
||||
mf (S n') = mf n' + S (2 * n').
|
||||
|
||||
Theorem there_is_at_most_one_mystery_function_04 :
|
||||
forall f g : nat -> nat,
|
||||
specification_of_mystery_function_04 f ->
|
||||
specification_of_mystery_function_04 g ->
|
||||
forall x : nat,
|
||||
f x = g x.
|
||||
Proof.
|
||||
intros f g.
|
||||
intros [S_f_0 S_f_n] [S_g_0 S_g_n].
|
||||
intro x.
|
||||
induction x as [| x' IHx'].
|
||||
- rewrite -> S_g_0.
|
||||
exact S_f_0.
|
||||
- rewrite -> (S_f_n x').
|
||||
rewrite -> (S_g_n x').
|
||||
rewrite -> IHx'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Definition unit_test_for_mystery_function_04 (mf : nat -> nat) :=
|
||||
(mf 1 =? 1)
|
||||
&& (mf 0 =? 0)
|
||||
&& (mf 2 =? 4)
|
||||
&& (mf 3 =? 9).
|
||||
|
||||
|
||||
Definition mystery_function_04 := Nat.square.
|
||||
|
||||
Compute (unit_test_for_mystery_function_04 mystery_function_04).
|
||||
|
||||
Theorem there_is_at_least_one_mystery_function_04 :
|
||||
specification_of_mystery_function_04 mystery_function_04.
|
||||
Proof.
|
||||
unfold specification_of_mystery_function_04, mystery_function_04.
|
||||
unfold Nat.square.
|
||||
split.
|
||||
- exact (Nat.mul_1_r 0).
|
||||
- intros n.
|
||||
Search (S _ * _).
|
||||
rewrite -> (Nat.mul_succ_l n (S n)).
|
||||
rewrite -> (Nat.mul_succ_r n n).
|
||||
Search (_ + S _).
|
||||
rewrite <- (Nat.add_assoc (n * n) n (S n)).
|
||||
rewrite -> (Nat.add_succ_r n n).
|
||||
Search (_ + _).
|
||||
rewrite <- (Nat.mul_1_l n) at 3.
|
||||
Search (_ * _ + _).
|
||||
rewrite <- (Nat.mul_succ_l 1 n).
|
||||
reflexivity.
|
||||
Qed.
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_15 (mf : nat -> nat * nat) :=
|
||||
mf 0 = (0, 1)
|
||||
/\
|
||||
forall n' : nat,
|
||||
mf (S n') = let (x, y) := mf n'
|
||||
in (S x, y * S x).
|
||||
|
||||
Theorem there_is_at_most_one_mystery_function_15 :
|
||||
forall f g : nat -> (nat * nat),
|
||||
specification_of_mystery_function_15 f ->
|
||||
specification_of_mystery_function_15 g ->
|
||||
forall x : nat,
|
||||
f x = g x.
|
||||
Proof.
|
||||
intros f g.
|
||||
intros [S_f_0 S_f_n] [S_g_0 S_g_n].
|
||||
intro x.
|
||||
induction x as [| x' IHx'].
|
||||
- rewrite -> S_g_0.
|
||||
exact S_f_0.
|
||||
- rewrite -> (S_f_n x').
|
||||
rewrite -> (S_g_n x').
|
||||
rewrite -> IHx'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Definition pair_equal (p1 p2: nat * nat) : bool :=
|
||||
match p1, p2 with
|
||||
| (a1, b1), (a2, b2) => (a1 =? a2) && (b1 =? b2)
|
||||
end.
|
||||
|
||||
Definition unit_test_for_mystery_function_15 (mf : nat -> nat * nat) :=
|
||||
(pair_equal (mf 0) (0, 1))
|
||||
&&
|
||||
(pair_equal (mf 1) (1, 1))
|
||||
&&
|
||||
(pair_equal (mf 2) (2, 2))
|
||||
&&
|
||||
(pair_equal (mf 3) (3, 6))
|
||||
&&
|
||||
(pair_equal (mf 4) (4, 24))
|
||||
&&
|
||||
(pair_equal (mf 5) (5, 120)).
|
||||
|
||||
(* The Factorial Function *)
|
||||
Fixpoint factorial (n : nat) :=
|
||||
match n with
|
||||
| 0 => (0, 1)
|
||||
| S k => match (factorial k) with
|
||||
| (a, b) => (n, n * b)
|
||||
end
|
||||
end.
|
||||
|
||||
Definition mystery_function_15 := factorial.
|
||||
|
||||
Compute (unit_test_for_mystery_function_15 mystery_function_15).
|
||||
|
||||
Theorem there_is_at_least_one_mystery_function_15 :
|
||||
specification_of_mystery_function_15 mystery_function_15.
|
||||
Proof.
|
||||
unfold specification_of_mystery_function_15, mystery_function_15.
|
||||
unfold factorial.
|
||||
split.
|
||||
- reflexivity.
|
||||
- intro n.
|
||||
induction n as [| n' IHn'].
|
||||
+ reflexivity.
|
||||
+ fold factorial in IHn'.
|
||||
fold factorial.
|
||||
rewrite -> IHn'.
|
||||
Abort.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_16 (mf : nat -> nat * nat) :=
|
||||
mf 0 = (0, 1)
|
||||
/\
|
||||
forall n' : nat,
|
||||
mf (S n') = let (x, y) := mf n'
|
||||
in (y, x + y).
|
||||
|
||||
Theorem there_is_at_most_one_mystery_function_16 :
|
||||
forall f g : nat -> (nat * nat),
|
||||
specification_of_mystery_function_16 f ->
|
||||
specification_of_mystery_function_16 g ->
|
||||
forall x : nat,
|
||||
f x = g x.
|
||||
Proof.
|
||||
intros f g.
|
||||
intros [S_f_0 S_f_n] [S_g_0 S_g_n].
|
||||
intro x.
|
||||
induction x as [| x' IHx'].
|
||||
- rewrite -> S_g_0.
|
||||
exact S_f_0.
|
||||
- rewrite -> (S_f_n x').
|
||||
rewrite -> (S_g_n x').
|
||||
rewrite -> IHx'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_17 (mf : nat -> nat) :=
|
||||
mf 0 = 0
|
||||
/\
|
||||
mf 1 = 1
|
||||
/\
|
||||
mf 2 = 1
|
||||
/\
|
||||
forall p q : nat,
|
||||
mf (S (p + q)) = mf (S p) * mf (S q) + mf p * mf q.
|
||||
|
||||
Theorem there_is_at_most_one_mystery_function_17 :
|
||||
forall f g : nat -> nat,
|
||||
specification_of_mystery_function_17 f ->
|
||||
specification_of_mystery_function_17 g ->
|
||||
forall x : nat,
|
||||
f x = g x.
|
||||
Proof.
|
||||
intros f g.
|
||||
intros [S_f_0 [S_f_1 [S_f_2 S_f_n]]].
|
||||
intros [S_g_0 [S_g_1 [S_g_2 S_g_n]]].
|
||||
intro x.
|
||||
induction x as [| x' IHx'].
|
||||
- rewrite -> S_g_0.
|
||||
exact S_f_0.
|
||||
- Search (_ + 1 = S _).
|
||||
(* Search (S _ + _). *)
|
||||
(* Check (plus_Sn_m 1 1). *)
|
||||
(* rewrite <- (Nat.add_1_l 2) at 1. *)
|
||||
(* rewrite <- (Nat.add_0_r 3). *)
|
||||
(* rewrite -> (plus_Sn_m 2 0). *)
|
||||
(* rewrite -> (S_mf_pq 1 1). *)
|
||||
(* rewrite -> (S_mf_pq 2 0). *)
|
||||
(* rewrite -> S_mf_2. *)
|
||||
(* rewrite -> S_mf_1. *)
|
||||
(* rewrite -> (S_mf_0). *)
|
||||
(* simpl. *)
|
||||
Abort.
|
||||
|
||||
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_18 (mf : nat -> nat) :=
|
||||
mf 0 = 0
|
||||
/\
|
||||
mf 1 = 1
|
||||
/\
|
||||
mf 2 = 1
|
||||
/\
|
||||
forall n''' : nat,
|
||||
mf n''' + mf (S (S (S n'''))) = 2 * mf (S (S n''')).
|
||||
|
||||
Theorem there_is_atmost_one_mystery_function_18 :
|
||||
forall f g : nat -> nat,
|
||||
specification_of_mystery_function_18 f ->
|
||||
specification_of_mystery_function_18 g ->
|
||||
forall x : nat,
|
||||
f x = g x.
|
||||
Proof.
|
||||
intros f g.
|
||||
intros [S_f_0 [S_f_1 [S_f_2 S_f_n]]].
|
||||
intros [S_g_0 [S_g_1 [S_g_2 S_g_n]]].
|
||||
intro x.
|
||||
induction x as [| x' IHx'].
|
||||
- rewrite -> S_g_0.
|
||||
exact S_f_0.
|
||||
- Search (S (S _) = S _).
|
||||
Abort.
|
||||
|
||||
|
||||
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Fixpoint add_v1 (i j : nat) : nat :=
|
||||
match i with
|
||||
| O =>
|
||||
j
|
||||
| S i' =>
|
||||
S (add_v1 i' j)
|
||||
end.
|
||||
|
||||
Definition specification_of_mystery_function_03 (mf : nat -> nat -> nat) :=
|
||||
mf 0 0 = 0
|
||||
/\
|
||||
(forall i j: nat, mf (S i) j = S (mf i j))
|
||||
/\
|
||||
(forall i j: nat, S (mf i j) = mf i (S j)).
|
||||
|
||||
Theorem there_is_at_least_one_mystery_function_03 :
|
||||
specification_of_mystery_function_03 Nat.add.
|
||||
Proof.
|
||||
unfold specification_of_mystery_function_03.
|
||||
split.
|
||||
- reflexivity.
|
||||
- split.
|
||||
+ intros i j.
|
||||
Search (S _ + _ = S (_ + _)).
|
||||
rewrite -> (plus_Sn_m i j).
|
||||
reflexivity.
|
||||
+ intros i j.
|
||||
rewrite <- (plus_n_Sm i j).
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Theorem there_is_atmost_one_mystery_function_03 :
|
||||
forall f g : nat -> nat -> nat,
|
||||
specification_of_mystery_function_03 f ->
|
||||
specification_of_mystery_function_03 g ->
|
||||
forall x y : nat,
|
||||
f x y = g x y.
|
||||
Proof.
|
||||
intros f g.
|
||||
intros [S_f_0 [S_f_1 S_f_2]].
|
||||
intros [S_g_0 [S_g_1 S_g_2]].
|
||||
induction x as [| x' IHx'].
|
||||
- intro y.
|
||||
Abort.
|
||||
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_42 (mf : nat -> nat) :=
|
||||
mf 1 = 42
|
||||
/\
|
||||
forall i j : nat,
|
||||
mf (i + j) = mf i + mf j.
|
||||
|
||||
Theorem there_is_atmost_one_mystery_function_42 :
|
||||
forall f g : nat -> nat,
|
||||
specification_of_mystery_function_42 f ->
|
||||
specification_of_mystery_function_42 g ->
|
||||
forall x : nat,
|
||||
f x = g x.
|
||||
Proof.
|
||||
intros f g.
|
||||
intros [S_f_1 S_f_S] [S_g_1 S_g_S].
|
||||
intro x.
|
||||
induction x as [| x' IHx'].
|
||||
- rewrite <- (Nat.add_0_l 0).
|
||||
rewrite -> (S_f_S 0 0).
|
||||
|
||||
Check Plus.plus_reg_l_stt.
|
||||
Abort.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_07 (mf : nat -> nat -> nat) :=
|
||||
(forall j : nat, mf 0 j = j)
|
||||
/\
|
||||
(forall i : nat, mf i 0 = i)
|
||||
/\
|
||||
(forall i j k : nat, mf (i + k) (j + k) = (mf i j) + k).
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_08 (mf : nat -> nat -> bool) :=
|
||||
(forall j : nat, mf 0 j = true)
|
||||
/\
|
||||
(forall i : nat, mf (S i) 0 = false)
|
||||
/\
|
||||
(forall i j : nat, mf (S i) (S j) = mf i j).
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_23 (mf : nat -> nat) :=
|
||||
mf 0 = 0
|
||||
/\
|
||||
mf 1 = 0
|
||||
/\
|
||||
forall n'' : nat,
|
||||
mf (S (S n'')) = S (mf n'').
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_24 (mf : nat -> nat) :=
|
||||
mf 0 = 0
|
||||
/\
|
||||
mf 1 = 1
|
||||
/\
|
||||
forall n'' : nat,
|
||||
mf (S (S n'')) = S (mf n'').
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_13 (mf : nat -> nat) :=
|
||||
(forall q : nat, mf (2 * q) = q)
|
||||
/\
|
||||
(forall q : nat, mf (S (2 * q)) = q).
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_25 (mf : nat -> nat) :=
|
||||
mf 0 = 0
|
||||
/\
|
||||
(forall q : nat,
|
||||
mf (2 * (S q)) = S (mf (S q)))
|
||||
/\
|
||||
mf 1 = 0
|
||||
/\
|
||||
(forall q : nat,
|
||||
mf (S (2 * (S q))) = S (mf (S q))).
|
||||
|
||||
(* ****** *)
|
||||
|
||||
Definition specification_of_mystery_function_20 (mf : nat -> nat -> nat) :=
|
||||
(forall j : nat, mf O j = j)
|
||||
/\
|
||||
(forall i j : nat, mf (S i) j = S (mf i j)).
|
||||
|
||||
(* ****** *)
|
||||
|
||||
Definition specification_of_mystery_function_21 (mf : nat -> nat -> nat) :=
|
||||
(forall j : nat, mf O j = j)
|
||||
/\
|
||||
(forall i j : nat, mf (S i) j = mf i (S j)).
|
||||
|
||||
(* ****** *)
|
||||
|
||||
Definition specification_of_mystery_function_22 (mf : nat -> nat -> nat) :=
|
||||
forall i j : nat,
|
||||
mf O j = j
|
||||
/\
|
||||
mf (S i) j = mf i (S j).
|
||||
|
||||
(* ********** *)
|
||||
|
||||
(* Binary trees of natural numbers: *)
|
||||
|
||||
Inductive tree : Type :=
|
||||
| Leaf : nat -> tree
|
||||
| Node : tree -> tree -> tree.
|
||||
|
||||
Definition specification_of_mystery_function_19 (mf : tree -> tree) :=
|
||||
(forall n : nat,
|
||||
mf (Leaf n) = Leaf n)
|
||||
/\
|
||||
(forall (n : nat) (t : tree),
|
||||
mf (Node (Leaf n) t) = Node (Leaf n) (mf t))
|
||||
/\
|
||||
(forall t11 t12 t2 : tree,
|
||||
mf (Node (Node t11 t12) t2) = mf (Node t11 (Node t12 t2))).
|
||||
|
||||
(* You might not manage to prove
|
||||
that at most one function satisfies this specification (why?),
|
||||
but consider whether the following function does.
|
||||
Assuming it does, what does this function do?
|
||||
And what is the issue here?
|
||||
*)
|
||||
|
||||
Fixpoint mystery_function_19_aux (t a : tree) : tree :=
|
||||
match t with
|
||||
| Leaf n =>
|
||||
Node (Leaf n) a
|
||||
| Node t1 t2 =>
|
||||
mystery_function_19_aux t1 (mystery_function_19_aux t2 a)
|
||||
end.
|
||||
|
||||
Fixpoint mystery_function_19 (t : tree) : tree :=
|
||||
match t with
|
||||
| Leaf n =>
|
||||
Leaf n
|
||||
| Node t1 t2 =>
|
||||
mystery_function_19_aux t1 (mystery_function_19 t2)
|
||||
end.
|
||||
|
||||
Theorem there_is_at_least_one_mystery_function :
|
||||
specification_of_mystery_function_19 mystery_function_19.
|
||||
Proof.
|
||||
unfold specification_of_mystery_function_19.
|
||||
unfold mystery_function_19.
|
||||
unfold mystery_function_19_aux.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_05 (mf : nat -> nat) :=
|
||||
mf 0 = 1
|
||||
/\
|
||||
forall i j : nat,
|
||||
mf (S (i + j)) = 2 * mf i * mf j.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_06 (mf : nat -> nat) :=
|
||||
mf 0 = 2
|
||||
/\
|
||||
forall i j : nat,
|
||||
mf (S (i + j)) = mf i * mf j.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_09 (mf : nat -> bool) :=
|
||||
mf 0 = false
|
||||
/\
|
||||
mf 1 = true
|
||||
/\
|
||||
forall i j : nat,
|
||||
mf (i + j) = xorb (mf i) (mf j).
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_10 (mf : nat -> bool) :=
|
||||
mf 0 = false
|
||||
/\
|
||||
mf 1 = true
|
||||
/\
|
||||
forall i j : nat,
|
||||
mf (i + j) = Bool.eqb (mf i) (mf j).
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_12 (mf : nat -> nat) :=
|
||||
mf 1 = 1
|
||||
/\
|
||||
forall i : nat,
|
||||
mf (S (S i)) = (S (S i)) * mf (S i).
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_14 (mf : nat -> bool) :=
|
||||
(forall q : nat, mf (2 * q) = true)
|
||||
/\
|
||||
(forall q : nat, mf (S (2 * q)) = false).
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition specification_of_mystery_function_29 (mf : nat -> bool) :=
|
||||
(mf 0 = true)
|
||||
/\
|
||||
(mf 1 = false)
|
||||
/\
|
||||
(forall n'' : nat, mf (S (S n'')) = mf n'').
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Require Import String.
|
||||
|
||||
Inductive arithmetic_expression : Type :=
|
||||
Literal : nat -> arithmetic_expression
|
||||
| Error : string -> arithmetic_expression
|
||||
| Plus : arithmetic_expression -> arithmetic_expression -> arithmetic_expression.
|
||||
|
||||
Inductive expressible_value : Type :=
|
||||
Expressible_nat : nat -> expressible_value
|
||||
| Expressible_msg : string -> expressible_value.
|
||||
|
||||
Definition specification_of_mystery_function_30 (mf : arithmetic_expression -> expressible_value) :=
|
||||
(forall n : nat,
|
||||
mf (Literal n) = Expressible_nat n)
|
||||
/\
|
||||
(forall s : string,
|
||||
mf (Error s) = Expressible_msg s)
|
||||
/\
|
||||
((forall (ae1 ae2 : arithmetic_expression)
|
||||
(n1 n2 : nat),
|
||||
mf ae1 = Expressible_nat n1 ->
|
||||
mf ae2 = Expressible_nat n2 ->
|
||||
mf (Plus ae1 ae2) = Expressible_nat (n1 + n2))
|
||||
/\
|
||||
(forall (ae1 ae2 : arithmetic_expression)
|
||||
(s1 : string),
|
||||
mf ae1 = Expressible_msg s1 ->
|
||||
mf (Plus ae1 ae2) = Expressible_msg s1)
|
||||
/\
|
||||
(forall (ae1 ae2 : arithmetic_expression)
|
||||
(s2 : string),
|
||||
mf ae2 = Expressible_msg s2 ->
|
||||
mf (Plus ae1 ae2) = Expressible_msg s2)).
|
||||
Abort.
|
||||
|
||||
Theorem there_is_at_most_one_mystery_function_30 :
|
||||
forall f g : arithmetic_expression -> expressible_value,
|
||||
specification_of_mystery_function_30 f ->
|
||||
specification_of_mystery_function_30 g ->
|
||||
forall expr : arithmetic_expression,
|
||||
f expr = g expr.
|
||||
Proof.
|
||||
intros f g.
|
||||
intros S_f.
|
||||
intros S_g.
|
||||
intro expr.
|
||||
induction expr as [n' | s' | e1 IHe1 e2 IHe2].
|
||||
- unfold specification_of_mystery_function_30 in S_f.
|
||||
destruct S_f as [S_f_literal _].
|
||||
unfold specification_of_mystery_function_30 in S_g.
|
||||
destruct S_g as [S_g_literal _].
|
||||
rewrite -> (S_g_literal n').
|
||||
exact (S_f_literal n').
|
||||
- unfold specification_of_mystery_function_30 in S_f.
|
||||
destruct S_f as [_ [S_f_error _]].
|
||||
unfold specification_of_mystery_function_30 in S_g.
|
||||
destruct S_g as [_ [S_g_error _]].
|
||||
rewrite -> (S_g_error s').
|
||||
exact (S_f_error s').
|
||||
- revert S_f.
|
||||
revert S_g.
|
||||
unfold specification_of_mystery_function_30.
|
||||
Abort.
|
||||
(* ********** *)
|
||||
|
||||
(* Simple examples of specifications: *)
|
||||
|
||||
(* ***** *)
|
||||
|
||||
Definition specification_of_the_factorial_function (fac : nat -> nat) :=
|
||||
fac 0 = 1
|
||||
/\
|
||||
forall n' : nat, fac (S n') = S n' * fac n'.
|
||||
|
||||
(* ***** *)
|
||||
|
||||
Definition specification_of_the_fibonacci_function (fib : nat -> nat) :=
|
||||
fib 0 = 0
|
||||
/\
|
||||
fib 1 = 1
|
||||
/\
|
||||
forall n'' : nat,
|
||||
fib (S (S n'')) = fib n'' + fib (S n'').
|
||||
|
||||
(* ********** *)
|
||||
|
||||
(* end of week-05_mystery-functions.v *)
|
||||
|
||||
|
||||
Search Prop.
|
||||
Loading…
Reference in New Issue
Block a user