feat: add finals questions
This commit is contained in:
parent
8948274c56
commit
5a12f23e7c
621
cs3234/labs/question-for-Yadunand.v
Normal file
621
cs3234/labs/question-for-Yadunand.v
Normal file
@ -0,0 +1,621 @@
|
||||
(* question-for-Yadunand.v *)
|
||||
(* CS3234 oral exam *)
|
||||
(* Sun 05 May 2024 *)
|
||||
|
||||
(* ********** *)
|
||||
|
||||
(* Your oral exam is about primitive recursion for Peano numbers. *)
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
|
||||
|
||||
Require Import Arith Bool List.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
(* Reminder:
|
||||
Any function that is expressible as an instance of nat_fold_right is said to be "primitive iterative". *)
|
||||
|
||||
Fixpoint nat_fold_right (V : Type) (zero_case : V) (succ_case : V -> V) (n : nat) : V :=
|
||||
match n with
|
||||
O =>
|
||||
zero_case
|
||||
| S n' =>
|
||||
succ_case (nat_fold_right V zero_case succ_case n')
|
||||
end.
|
||||
|
||||
(* Definition:
|
||||
Any function that is expressible as an instance of nat_parafold_right is said to be "primitive recursive". *)
|
||||
|
||||
Fixpoint nat_parafold_right (V : Type) (zero_case : V) (succ_case : nat -> V -> V) (n : nat) : V := match n with
|
||||
O =>
|
||||
zero_case
|
||||
| S n' =>
|
||||
succ_case n' (nat_parafold_right V zero_case succ_case n')
|
||||
end.
|
||||
|
||||
Lemma fold_unfold_nat_parafold_right_O :
|
||||
forall (V : Type)
|
||||
(zero_case : V)
|
||||
(succ_case : nat -> V -> V),
|
||||
nat_parafold_right V zero_case succ_case 0 =
|
||||
zero_case.
|
||||
Proof.
|
||||
fold_unfold_tactic nat_parafold_right.
|
||||
Qed.
|
||||
|
||||
Lemma fold_unfold_nat_parafold_right_S :
|
||||
forall (V : Type)
|
||||
(zero_case : V)
|
||||
(succ_case : nat -> V -> V)
|
||||
(n' : nat),
|
||||
nat_parafold_right V zero_case succ_case (S n') =
|
||||
succ_case n' (nat_parafold_right V zero_case succ_case n').
|
||||
Proof.
|
||||
fold_unfold_tactic nat_parafold_right.
|
||||
Qed.
|
||||
|
||||
(* ***** *)
|
||||
|
||||
Fixpoint nat_parafold_left (V : Type) (zero_case : V) (succ_case : nat -> V -> V) (n : nat) : V :=
|
||||
match n with
|
||||
O =>
|
||||
zero_case
|
||||
| S n' =>
|
||||
nat_parafold_left V (succ_case n' zero_case) succ_case n'
|
||||
end.
|
||||
|
||||
Lemma fold_unfold_nat_parafold_left_O :
|
||||
forall (V : Type)
|
||||
(zero_case : V)
|
||||
(succ_case : nat -> V -> V),
|
||||
nat_parafold_left V zero_case succ_case 0 =
|
||||
zero_case.
|
||||
Proof.
|
||||
fold_unfold_tactic nat_parafold_left.
|
||||
Qed.
|
||||
|
||||
Lemma fold_unfold_nat_parafold_left_S :
|
||||
forall (V : Type)
|
||||
(zero_case : V)
|
||||
(succ_case : nat -> V -> V)
|
||||
(n' : nat),
|
||||
nat_parafold_left V zero_case succ_case (S n') =
|
||||
nat_parafold_left V (succ_case n' zero_case) succ_case n'.
|
||||
Proof.
|
||||
fold_unfold_tactic nat_parafold_left.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition test_fac (candidate: nat -> nat) : bool :=
|
||||
(Nat.eqb (candidate 0) 1)
|
||||
&&
|
||||
(Nat.eqb (candidate 5) 120).
|
||||
|
||||
(* ***** *)
|
||||
|
||||
(* Recursive implementation of the factorial function: *)
|
||||
|
||||
Fixpoint r_fac (n : nat) : nat :=
|
||||
match n with
|
||||
O =>
|
||||
1
|
||||
| S n' =>
|
||||
S n' * r_fac n'
|
||||
end.
|
||||
|
||||
Compute (test_fac r_fac).
|
||||
|
||||
(* 1.a Implement r_fac as an instance of nat_parafold_right: *)
|
||||
|
||||
Definition r_fac_right (n : nat) : nat :=
|
||||
nat_parafold_right nat 1 (fun n' ih => (S n') * ih) n.
|
||||
|
||||
(* 1.b Test your implementation. *)
|
||||
Compute (test_fac r_fac).
|
||||
|
||||
(* 1.c Prove that r_fac and r_fac_right are equivalent. *)
|
||||
|
||||
Lemma fold_unfold_r_fac_O :
|
||||
r_fac 0 = 1.
|
||||
Proof.
|
||||
fold_unfold_tactic r_fac.
|
||||
Qed.
|
||||
Lemma fold_unfold_r_fac_S :
|
||||
forall (n' : nat),
|
||||
r_fac (S n') = S n' * r_fac n'.
|
||||
Proof.
|
||||
fold_unfold_tactic r_fac.
|
||||
Qed.
|
||||
|
||||
Lemma about_r_fac_and_r_fac_right :
|
||||
forall (n : nat),
|
||||
r_fac n = nat_parafold_right nat 1 (fun n' ih : nat => S n' * ih) n.
|
||||
Proof.
|
||||
intro n.
|
||||
induction n as [ | n' IHn' ].
|
||||
- rewrite -> fold_unfold_r_fac_O.
|
||||
rewrite -> fold_unfold_nat_parafold_right_O.
|
||||
reflexivity.
|
||||
- rewrite -> fold_unfold_r_fac_S.
|
||||
rewrite -> fold_unfold_nat_parafold_right_S.
|
||||
rewrite <- IHn'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Theorem r_fac_and_r_fac_right_are_equivalent :
|
||||
forall (n : nat),
|
||||
r_fac n = r_fac_right n.
|
||||
Proof.
|
||||
intro n.
|
||||
unfold r_fac_right.
|
||||
exact (about_r_fac_and_r_fac_right n).
|
||||
Qed.
|
||||
|
||||
(* ***** *)
|
||||
|
||||
(* Tail-recursive implementation of the factorial function: *)
|
||||
|
||||
Fixpoint tr_fac_acc (n a : nat) : nat :=
|
||||
match n with
|
||||
O =>
|
||||
a
|
||||
| S n' =>
|
||||
tr_fac_acc n' (S n' * a)
|
||||
end.
|
||||
|
||||
Lemma fold_unfold_tr_fac_acc_O :
|
||||
forall (a : nat),
|
||||
tr_fac_acc 0 a = a.
|
||||
Proof.
|
||||
fold_unfold_tactic r_fac.
|
||||
Qed.
|
||||
|
||||
Lemma fold_unfold_tr_fac_acc_S :
|
||||
forall (n' a : nat),
|
||||
tr_fac_acc (S n') a = tr_fac_acc n' (S n' * a).
|
||||
Proof.
|
||||
fold_unfold_tactic r_fac.
|
||||
Qed.
|
||||
|
||||
Definition tr_fac (n : nat) : nat :=
|
||||
tr_fac_acc n 1.
|
||||
|
||||
Compute (test_fac tr_fac).
|
||||
|
||||
(* 2.a Implement tr_fac as an instance of nat_parafold_left: *)
|
||||
|
||||
Definition tr_fac_left (n : nat) : nat :=
|
||||
nat_parafold_left nat 1 (fun n' a => S n' * a) n.
|
||||
|
||||
(* 2.b Test your implementation. *)
|
||||
|
||||
Compute (test_fac tr_fac_left).
|
||||
|
||||
(* 2.c Prove that tr_fac and tr_fac_left are equivalent. *)
|
||||
(* Lemma about_tr_fac_acc : *)
|
||||
(* forall (n a : nat), *)
|
||||
(* tr_fac_acc n a = (tr_fac_acc n 1) * a. *)
|
||||
(* Proof. *)
|
||||
(* intros n. *)
|
||||
(* induction n as [ | n' IHn' ]. *)
|
||||
(* - intro a. *)
|
||||
(* rewrite -> fold_unfold_tr_fac_acc_O. *)
|
||||
(* rewrite -> fold_unfold_tr_fac_acc_O. *)
|
||||
(* rewrite -> Nat.mul_1_l. *)
|
||||
(* reflexivity. *)
|
||||
(* - intro a. *)
|
||||
(* rewrite -> fold_unfold_tr_fac_acc_S. *)
|
||||
(* rewrite -> (IHn' (S (S n') * a)). *)
|
||||
(* rewrite -> *)
|
||||
|
||||
|
||||
Lemma about_tr_fac_and_tr_fac_left :
|
||||
forall (n : nat),
|
||||
tr_fac_acc n 1 = nat_parafold_left nat 1 (fun n' a : nat => S n' * a) n.
|
||||
Proof.
|
||||
intro n.
|
||||
induction n as [ | n' IHn' ].
|
||||
- rewrite -> fold_unfold_tr_fac_acc_O.
|
||||
rewrite -> fold_unfold_nat_parafold_left_O.
|
||||
reflexivity.
|
||||
- rewrite -> fold_unfold_tr_fac_acc_S.
|
||||
rewrite -> fold_unfold_nat_parafold_left_S.
|
||||
rewrite -> Nat.mul_1_r.
|
||||
Abort.
|
||||
|
||||
Lemma about_tr_fac_and_tr_fac_left :
|
||||
forall (n a: nat),
|
||||
tr_fac_acc n a = nat_parafold_left nat a (fun n' a : nat => S n' * a) n.
|
||||
Proof.
|
||||
intro n.
|
||||
induction n as [ | n' IHn' ].
|
||||
- intro a.
|
||||
rewrite -> fold_unfold_tr_fac_acc_O.
|
||||
rewrite -> fold_unfold_nat_parafold_left_O.
|
||||
reflexivity.
|
||||
- intro a.
|
||||
rewrite -> fold_unfold_tr_fac_acc_S.
|
||||
rewrite -> fold_unfold_nat_parafold_left_S.
|
||||
exact (IHn' (S n' * a)).
|
||||
Qed.
|
||||
|
||||
Theorem tr_fac_and_tr_fac_left_are_equivalent :
|
||||
forall (n : nat),
|
||||
tr_fac n = tr_fac_left n.
|
||||
Proof.
|
||||
intro n.
|
||||
unfold tr_fac.
|
||||
unfold tr_fac_left.
|
||||
exact (about_tr_fac_and_tr_fac_left n 1).
|
||||
Qed.
|
||||
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition test_Sigma (candidate: nat -> (nat -> nat) -> nat) : bool :=
|
||||
(Nat.eqb (candidate 0 (fun n => S (2 * n))) 1)
|
||||
&&
|
||||
(Nat.eqb (candidate 1 (fun n => S (2 * n))) 4)
|
||||
&&
|
||||
(Nat.eqb (candidate 2 (fun n => S (2 * n))) 9)
|
||||
&&
|
||||
(Nat.eqb (candidate 3 (fun n => S (2 * n))) 16).
|
||||
|
||||
(* ***** *)
|
||||
|
||||
(* Recursive implementation of the summation function: *)
|
||||
|
||||
Fixpoint r_Sigma (n : nat) (f : nat -> nat) : nat :=
|
||||
match n with
|
||||
O =>
|
||||
f 0
|
||||
| S n' =>
|
||||
(r_Sigma n' f) + f (S n')
|
||||
end.
|
||||
|
||||
Compute (test_Sigma r_Sigma).
|
||||
|
||||
(* 3.a Implement r_Sigma as an instance of nat_parafold_right: *)
|
||||
|
||||
Definition r_Sigma_right (n : nat) (f : nat -> nat) : nat :=
|
||||
nat_parafold_right
|
||||
nat
|
||||
(f 0)
|
||||
(fun n' ih => (ih + f (S n')))
|
||||
n.
|
||||
|
||||
(* 3.b Test your implementation. *)
|
||||
|
||||
Compute (test_Sigma r_Sigma_right).
|
||||
|
||||
(* 3.c Prove that r_Sigma and r_Sigma_right are equivalent. *)
|
||||
|
||||
Lemma fold_unfold_r_Sigma_O :
|
||||
forall (f : nat -> nat),
|
||||
r_Sigma O f = f 0.
|
||||
Proof.
|
||||
fold_unfold_tactic r_Sigma.
|
||||
Qed.
|
||||
Lemma fold_unfold_r_Sigma_S :
|
||||
forall (n' : nat)
|
||||
(f : nat -> nat),
|
||||
r_Sigma (S n') f = (r_Sigma n' f) + f (S n').
|
||||
Proof.
|
||||
fold_unfold_tactic r_Sigma.
|
||||
Qed.
|
||||
|
||||
Lemma about_r_Sigma_and_r_Sigma_right :
|
||||
forall (n : nat)
|
||||
(f : nat -> nat),
|
||||
r_Sigma n f = nat_parafold_right nat (f 0) (fun n' ih : nat => ih + f (S n')) n.
|
||||
Proof.
|
||||
intros n f.
|
||||
induction n as [ | n' IHn' ].
|
||||
- rewrite -> fold_unfold_r_Sigma_O.
|
||||
rewrite -> fold_unfold_nat_parafold_right_O.
|
||||
reflexivity.
|
||||
- rewrite -> fold_unfold_r_Sigma_S.
|
||||
rewrite -> fold_unfold_nat_parafold_right_S.
|
||||
rewrite <- IHn'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Theorem r_Sigma_and_r_Sigma_right_are_equivalent :
|
||||
forall (n : nat)
|
||||
(f : nat -> nat),
|
||||
r_Sigma n f = r_Sigma_right n f.
|
||||
Proof.
|
||||
intros n f.
|
||||
unfold r_Sigma_right.
|
||||
exact (about_r_Sigma_and_r_Sigma_right n f).
|
||||
Qed.
|
||||
|
||||
(* ***** *)
|
||||
|
||||
(* Tail-recursive implementation of the summation function: *)
|
||||
|
||||
Fixpoint tr_Sigma_acc (n : nat) (f : nat -> nat) (a : nat) : nat :=
|
||||
match n with
|
||||
O =>
|
||||
a
|
||||
| S n' =>
|
||||
tr_Sigma_acc n' f (a + f (S n'))
|
||||
end.
|
||||
|
||||
Lemma fold_unfold_tr_Sigma_acc_O :
|
||||
forall (f : nat -> nat)
|
||||
(a : nat),
|
||||
tr_Sigma_acc 0 f a = a.
|
||||
Proof.
|
||||
fold_unfold_tactic tr_Sigma_acc.
|
||||
Qed.
|
||||
Lemma fold_unfold_tr_Sigma_acc_S :
|
||||
forall (n' : nat)
|
||||
(f : nat -> nat)
|
||||
(a : nat),
|
||||
tr_Sigma_acc (S n') f a = tr_Sigma_acc n' f (a + f (S n')).
|
||||
Proof.
|
||||
fold_unfold_tactic tr_Sigma_acc.
|
||||
Qed.
|
||||
|
||||
Definition tr_Sigma (n : nat) (f : nat -> nat) : nat :=
|
||||
tr_Sigma_acc n f (f 0).
|
||||
|
||||
Compute (test_Sigma tr_Sigma).
|
||||
|
||||
(* 4.a Implement tr_Sigma as an instance of nat_parafold_left: *)
|
||||
|
||||
Definition tr_Sigma_left (n : nat) (f : nat -> nat) : nat :=
|
||||
nat_parafold_left nat (f 0) (fun n' a => a + f (S n')) n.
|
||||
|
||||
|
||||
(* 4.b Test your implementation. *)
|
||||
|
||||
Compute (test_Sigma tr_Sigma_left).
|
||||
|
||||
(* 4.c Prove that tr_Sigma and tr_Sigma_left are equivalent. *)
|
||||
|
||||
Lemma about_tr_Sigma_and_tr_Sigma_left :
|
||||
forall (n : nat)
|
||||
(f : nat -> nat),
|
||||
tr_Sigma_acc n f (f 0) = nat_parafold_left nat (f 0) (fun n' a : nat => a + f (S n')) n.
|
||||
Proof.
|
||||
Abort.
|
||||
|
||||
Lemma about_tr_Sigma_and_tr_Sigma_left :
|
||||
forall (n: nat)
|
||||
(f : nat -> nat)
|
||||
(a : nat),
|
||||
tr_Sigma_acc n f a = nat_parafold_left nat a (fun n' a : nat => a + f (S n')) n.
|
||||
Proof.
|
||||
intros n f.
|
||||
induction n as [ | n' IHn' ].
|
||||
- intros a.
|
||||
rewrite -> (fold_unfold_tr_Sigma_acc_O f a).
|
||||
rewrite -> fold_unfold_nat_parafold_left_O.
|
||||
reflexivity.
|
||||
- intros a.
|
||||
rewrite -> (fold_unfold_tr_Sigma_acc_S n' f a).
|
||||
rewrite -> fold_unfold_nat_parafold_left_S.
|
||||
exact (IHn' (a + f (S n'))).
|
||||
Qed.
|
||||
|
||||
Theorem tr_Sigma_and_tr_Sigma_left_are_equivalent :
|
||||
forall (n : nat)
|
||||
(f : nat -> nat),
|
||||
tr_Sigma n f = tr_Sigma_left n f.
|
||||
Proof.
|
||||
intros n f.
|
||||
unfold tr_Sigma,tr_Sigma_left.
|
||||
exact (about_tr_Sigma_and_tr_Sigma_left n f (f 0)).
|
||||
Qed.
|
||||
(* ********** *)
|
||||
|
||||
(* 5. Taking inspiration from the theorem about folding left and right over lists in the midterm project,
|
||||
state and admit a similar theorem about parafolding left and right over Peano numbers. *)
|
||||
|
||||
(* Theorem folding_left_and_right_over_lists : *)
|
||||
(* forall (V W : Type) *)
|
||||
(* (cons_case : V -> W -> W), *)
|
||||
(* is_left_permutative V W cons_case -> *)
|
||||
(* forall (nil_case : W) *)
|
||||
(* (vs : list V), *)
|
||||
(* list_fold_left V W nil_case cons_case vs = *)
|
||||
(* list_fold_right V W nil_case cons_case vs. *)
|
||||
(* Proof. *)
|
||||
(* intros V W cons_case. *)
|
||||
(* unfold is_left_permutative. *)
|
||||
(* intros H_left_permutative nil_case vs. *)
|
||||
(* induction vs as [ | v' vs' IHvs']. *)
|
||||
(* - rewrite -> (fold_unfold_list_fold_left_nil V W nil_case cons_case). *)
|
||||
(* rewrite -> (fold_unfold_list_fold_right_nil V W nil_case cons_case). *)
|
||||
(* reflexivity. *)
|
||||
(* - rewrite -> (fold_unfold_list_fold_left_cons V W nil_case cons_case v' vs'). *)
|
||||
(* rewrite -> (fold_unfold_list_fold_right_cons V W nil_case cons_case v' vs'). *)
|
||||
(* rewrite <- IHvs'. *)
|
||||
(* rewrite -> (about_list_fold_left_with_left_permutative_cons_case *)
|
||||
(* V W cons_case H_left_permutative nil_case v' vs'). *)
|
||||
(* reflexivity. *)
|
||||
(* Qed. *)
|
||||
(* Definition is_left_permutative (V W : Type) (op2 : V -> W -> W) := *)
|
||||
(* forall (v1 v2 : V) *)
|
||||
(* (w : W), *)
|
||||
(* op2 v1 (op2 v2 w) = op2 v2 (op2 v1 w). *)
|
||||
(* ********** *)
|
||||
|
||||
Definition is_left_permutative (V : Type) (op2 : nat -> V -> V) :=
|
||||
forall (n1 n2 : nat)
|
||||
(v : V),
|
||||
op2 n1 (op2 n2 v) = op2 n2 (op2 n1 v).
|
||||
|
||||
Lemma about_parafolding_l_over_peano_numbers :
|
||||
forall (V: Type)
|
||||
(succ_case : nat -> V -> V),
|
||||
is_left_permutative V succ_case ->
|
||||
forall (n : nat)
|
||||
(zero_case : V),
|
||||
nat_parafold_left V (succ_case n zero_case) succ_case n =
|
||||
succ_case n (nat_parafold_left V zero_case succ_case n).
|
||||
Proof.
|
||||
intros V succ_case H_is_left_permutative n.
|
||||
unfold is_left_permutative in H_is_left_permutative.
|
||||
induction n as [| n' IHn'].
|
||||
- intro zero_case.
|
||||
rewrite -> 2 fold_unfold_nat_parafold_left_O.
|
||||
reflexivity.
|
||||
- intro zero_case.
|
||||
rewrite -> fold_unfold_nat_parafold_left_S.
|
||||
rewrite ->H_is_left_permutative.
|
||||
Abort. (* The lemma I stated here is a bit wrong. *)
|
||||
|
||||
Lemma about_parafolding_left_over_peano_numbers :
|
||||
forall (V: Type)
|
||||
(succ_case : nat -> V -> V),
|
||||
is_left_permutative V succ_case ->
|
||||
forall (n m : nat)
|
||||
(zero_case : V),
|
||||
nat_parafold_left V (succ_case m zero_case) succ_case n =
|
||||
succ_case m (nat_parafold_left V zero_case succ_case n).
|
||||
Proof.
|
||||
intros V succ_case H_is_left_permutative n m.
|
||||
unfold is_left_permutative in H_is_left_permutative.
|
||||
induction n as [| n' IHn'].
|
||||
- intros zero_case.
|
||||
rewrite -> 2 fold_unfold_nat_parafold_left_O.
|
||||
reflexivity.
|
||||
- intros zero_case.
|
||||
rewrite -> fold_unfold_nat_parafold_left_S.
|
||||
rewrite -> H_is_left_permutative.
|
||||
rewrite -> (IHn' (succ_case n' zero_case)).
|
||||
rewrite -> fold_unfold_nat_parafold_left_S.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Lemma about_parafolding_right_over_peano_numbers :
|
||||
forall (V : Type)
|
||||
(succ_case : nat -> V -> V),
|
||||
is_left_permutative V succ_case ->
|
||||
forall (n m : nat)
|
||||
(zero_case : V),
|
||||
nat_parafold_right V (succ_case m zero_case) succ_case n =
|
||||
succ_case m (nat_parafold_right V zero_case succ_case n).
|
||||
Proof.
|
||||
intros V succ_case H_left_permutative n m zero_case.
|
||||
unfold is_left_permutative in H_left_permutative.
|
||||
induction n as [ | n' IHn' ].
|
||||
- rewrite -> 2 fold_unfold_nat_parafold_right_O.
|
||||
reflexivity.
|
||||
- rewrite -> 2 fold_unfold_nat_parafold_right_S.
|
||||
rewrite -> H_left_permutative.
|
||||
rewrite -> IHn'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
Theorem parafolding_left_and_right_over_peano_numbers :
|
||||
forall (V : Type)
|
||||
(succ_case : nat -> V -> V),
|
||||
is_left_permutative V succ_case ->
|
||||
forall (n : nat)
|
||||
(zero_case : V),
|
||||
nat_parafold_left V zero_case succ_case n = nat_parafold_right V zero_case succ_case n.
|
||||
Proof.
|
||||
intros V succ_case H_left_permutative n zero_case.
|
||||
(* Generalizing the accumulator(?) *)
|
||||
induction n as [ | n' IHn' ].
|
||||
- rewrite -> fold_unfold_nat_parafold_left_O.
|
||||
rewrite -> fold_unfold_nat_parafold_right_O.
|
||||
reflexivity.
|
||||
- rewrite -> fold_unfold_nat_parafold_left_S.
|
||||
rewrite -> fold_unfold_nat_parafold_right_S.
|
||||
rewrite <- IHn'.
|
||||
Check (about_parafolding_left_over_peano_numbers V succ_case H_left_permutative n' n' zero_case).
|
||||
exact (about_parafolding_left_over_peano_numbers V succ_case H_left_permutative n' n' zero_case).
|
||||
Restart.
|
||||
intros V succ_case H_left_permutative n.
|
||||
(* Generalizing the accumulator(?) *)
|
||||
induction n as [ | n' IHn' ].
|
||||
- intro zero_case.
|
||||
rewrite -> fold_unfold_nat_parafold_left_O.
|
||||
rewrite -> fold_unfold_nat_parafold_right_O.
|
||||
reflexivity.
|
||||
- intro zero_case.
|
||||
rewrite -> fold_unfold_nat_parafold_right_S.
|
||||
rewrite -> fold_unfold_nat_parafold_left_S.
|
||||
rewrite -> (IHn' (succ_case n' zero_case)).
|
||||
exact (about_parafolding_right_over_peano_numbers
|
||||
V
|
||||
succ_case
|
||||
H_left_permutative
|
||||
n'
|
||||
n'
|
||||
zero_case
|
||||
).
|
||||
Qed.
|
||||
|
||||
(* 6. As a corollary of your similar theorem,
|
||||
prove that tr_fac_left and r_fac_right are equivalent
|
||||
and that tr_Sigma_left and r_Sigma_right are equivalent. *)
|
||||
|
||||
Lemma succ_case_of_fac_is_left_permutative :
|
||||
is_left_permutative nat (fun n' a : nat => S n' * a).
|
||||
Proof.
|
||||
unfold is_left_permutative.
|
||||
intros n1 n2 v.
|
||||
rewrite -> Nat.mul_shuffle3.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Corollary tr_fac_left_and_r_fac_right_are_equivalent :
|
||||
forall (n : nat),
|
||||
tr_fac_left n = r_fac_right n.
|
||||
Proof.
|
||||
intros n.
|
||||
unfold tr_fac_left.
|
||||
unfold r_fac_right.
|
||||
exact (parafolding_left_and_right_over_peano_numbers
|
||||
nat
|
||||
(fun n' a : nat => S n' * a)
|
||||
succ_case_of_fac_is_left_permutative
|
||||
n
|
||||
1
|
||||
).
|
||||
Qed.
|
||||
|
||||
Lemma succ_case_of_Sigma_is_left_permutative :
|
||||
forall (f : nat -> nat),
|
||||
is_left_permutative nat (fun n' a : nat => a + f (S n')).
|
||||
Proof.
|
||||
intro f.
|
||||
unfold is_left_permutative.
|
||||
intros n1 n2 v.
|
||||
Search (_ + _ + _).
|
||||
rewrite -> Nat.add_shuffle0.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Corollary tr_Sigma_left_and_r_Sigma_right_are_equivalent :
|
||||
forall (n : nat)
|
||||
(f : nat -> nat),
|
||||
|
||||
tr_Sigma_left n f = r_Sigma_right n f.
|
||||
Proof.
|
||||
intros n f.
|
||||
unfold tr_Sigma_left.
|
||||
unfold r_Sigma_right.
|
||||
exact (parafolding_left_and_right_over_peano_numbers
|
||||
nat
|
||||
(fun n' a : nat => a + f (S n'))
|
||||
(succ_case_of_Sigma_is_left_permutative f)
|
||||
n
|
||||
(f 0)
|
||||
).
|
||||
Qed.
|
||||
(* ********** *)
|
||||
|
||||
(* 7. Prove your similar theorem. *)
|
||||
|
||||
(* ********** *)
|
||||
|
||||
(* end of question-for-Yadunand.v *)
|
||||
@ -1536,9 +1536,41 @@ Proof.
|
||||
rewrite -> (S_run_one bcis n H_fdel_one).
|
||||
reflexivity. }
|
||||
split.
|
||||
{ intros n n' H_fdel_many.
|
||||
rewrite -> (S_run_many bcis n n' H_fdel_many).
|
||||
{ intros n n' ds'' H_fdel_many.
|
||||
rewrite -> (S_run_many bcis n n' ds'' H_fdel_many ).
|
||||
reflexivity. }
|
||||
intros s H_fdel_KO.
|
||||
rewrite -> (S_run_KO bcis s H_fdel_KO).
|
||||
reflexivity.
|
||||
- intro S_run.
|
||||
assert (S_run := S_run fetch_decode_execute_loop fetch_decode_execute_loop_satifies_the_specification).
|
||||
intros fdel S_fdel.
|
||||
split.
|
||||
{ intros bcis H_fdel_nil.
|
||||
rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis) in H_fdel_nil.
|
||||
destruct (S_run bcis) as [S_run_nil _].
|
||||
rewrite -> (S_run_nil H_fdel_nil).
|
||||
reflexivity.
|
||||
}
|
||||
split.
|
||||
{ intros bcis n H_fdel_one.
|
||||
rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis) in H_fdel_one.
|
||||
destruct (S_run bcis) as [_ [S_run_one _]].
|
||||
rewrite -> (S_run_one n H_fdel_one).
|
||||
reflexivity.
|
||||
}
|
||||
split.
|
||||
{ intros bcis n n' ds'' H_fdel_many.
|
||||
rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis) in H_fdel_many.
|
||||
destruct (S_run bcis) as [_ [_ [S_run_many _]]].
|
||||
rewrite -> (S_run_many n n' ds'' H_fdel_many).
|
||||
reflexivity.
|
||||
}
|
||||
intros bcis s H_fdel_KO.
|
||||
rewrite -> (there_is_at_most_one_fetch_decode_execute_loop fdel fetch_decode_execute_loop S_fdel fetch_decode_execute_loop_satifies_the_specification bcis) in H_fdel_KO.
|
||||
destruct (S_run bcis) as [_ [_ [_ S_run_KO]]].
|
||||
rewrite -> (S_run_KO s H_fdel_KO).
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* end of term-project.v *)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user