258 lines
6.4 KiB
Coq
258 lines
6.4 KiB
Coq
Set Warnings "-notation-overridden,-parsing".
|
|
From Stdlib Require Export String.
|
|
From LF Require Import Induction.
|
|
|
|
Parameter MISSING: Type.
|
|
|
|
Module Check.
|
|
|
|
Ltac check_type A B :=
|
|
match type of A with
|
|
| context[MISSING] => idtac "Missing:" A
|
|
| ?T => first [unify T B; idtac "Type: ok" | idtac "Type: wrong - should be (" B ")"]
|
|
end.
|
|
|
|
Ltac print_manual_grade A :=
|
|
match eval compute in A with
|
|
| Some (_ ?S ?C) =>
|
|
idtac "Score:" S;
|
|
match eval compute in C with
|
|
| ""%string => idtac "Comment: None"
|
|
| _ => idtac "Comment:" C
|
|
end
|
|
| None =>
|
|
idtac "Score: Ungraded";
|
|
idtac "Comment: None"
|
|
end.
|
|
|
|
End Check.
|
|
|
|
From LF Require Import Induction.
|
|
Import Check.
|
|
|
|
Goal True.
|
|
|
|
idtac "------------------- basic_induction --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> mul_0_r".
|
|
idtac "Possible points: 0.5".
|
|
check_type @mul_0_r ((forall n : nat, @eq nat (Nat.mul n 0) 0)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions mul_0_r.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> plus_n_Sm".
|
|
idtac "Possible points: 0.5".
|
|
check_type @plus_n_Sm ((forall n m : nat, @eq nat (S (Nat.add n m)) (Nat.add n (S m)))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions plus_n_Sm.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> add_comm".
|
|
idtac "Possible points: 0.5".
|
|
check_type @add_comm ((forall n m : nat, @eq nat (Nat.add n m) (Nat.add m n))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions add_comm.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> add_assoc".
|
|
idtac "Possible points: 0.5".
|
|
check_type @add_assoc (
|
|
(forall n m p : nat,
|
|
@eq nat (Nat.add n (Nat.add m p)) (Nat.add (Nat.add n m) p))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions add_assoc.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- double_plus --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> double_plus".
|
|
idtac "Possible points: 2".
|
|
check_type @double_plus ((forall n : nat, @eq nat (double n) (Nat.add n n))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions double_plus.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- eqb_refl --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> eqb_refl".
|
|
idtac "Possible points: 2".
|
|
check_type @eqb_refl ((forall n : nat, @eq bool (eqb n n) true)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions eqb_refl.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- mul_comm --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> add_shuffle3".
|
|
idtac "Possible points: 1".
|
|
check_type @add_shuffle3 (
|
|
(forall n m p : nat,
|
|
@eq nat (Nat.add n (Nat.add m p)) (Nat.add m (Nat.add n p)))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions add_shuffle3.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> mul_comm".
|
|
idtac "Possible points: 2".
|
|
check_type @mul_comm ((forall m n : nat, @eq nat (Nat.mul m n) (Nat.mul n m))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions mul_comm.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- binary_commute --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> bin_to_nat_pres_incr".
|
|
idtac "Possible points: 3".
|
|
check_type @bin_to_nat_pres_incr (
|
|
(forall b : bin, @eq nat (bin_to_nat (incr b)) (Nat.add 1 (bin_to_nat b)))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions bin_to_nat_pres_incr.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- nat_bin_nat --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> nat_bin_nat".
|
|
idtac "Possible points: 3".
|
|
check_type @nat_bin_nat ((forall n : nat, @eq nat (bin_to_nat (nat_to_bin n)) n)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions nat_bin_nat.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- double_bin --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> double_incr".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 0.5".
|
|
check_type @double_incr ((forall n : nat, @eq nat (double (S n)) (S (S (double n))))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions double_incr.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> double_bin_zero".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 0.5".
|
|
check_type @double_bin_zero ((@eq bin (double_bin Z) Z)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions double_bin_zero.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> double_incr_bin".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 1".
|
|
check_type @double_incr_bin (
|
|
(forall b : bin, @eq bin (double_bin (incr b)) (incr (incr (double_bin b))))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions double_incr_bin.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- bin_nat_bin --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> bin_nat_bin".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 6".
|
|
check_type @bin_nat_bin (
|
|
(forall b : bin, @eq bin (nat_to_bin (bin_to_nat b)) (normalize b))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions bin_nat_bin.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac " ".
|
|
|
|
idtac "Max points - standard: 15".
|
|
idtac "Max points - advanced: 23".
|
|
idtac "".
|
|
idtac "Allowed Axioms:".
|
|
idtac "functional_extensionality".
|
|
idtac "FunctionalExtensionality.functional_extensionality_dep".
|
|
idtac "plus_le".
|
|
idtac "le_trans".
|
|
idtac "le_plus_l".
|
|
idtac "add_le_cases".
|
|
idtac "Sn_le_Sm__n_le_m".
|
|
idtac "O_le_n".
|
|
idtac "".
|
|
idtac "".
|
|
idtac "********** Summary **********".
|
|
idtac "".
|
|
idtac "Below is a summary of the automatically graded exercises that are incomplete.".
|
|
idtac "".
|
|
idtac "The output for each exercise can be any of the following:".
|
|
idtac " - 'Closed under the global context', if it is complete".
|
|
idtac " - 'MANUAL', if it is manually graded".
|
|
idtac " - A list of pending axioms, containing unproven assumptions. In this case".
|
|
idtac " the exercise is considered complete, if the axioms are all allowed.".
|
|
idtac "".
|
|
idtac "********** Standard **********".
|
|
idtac "---------- mul_0_r ---------".
|
|
Print Assumptions mul_0_r.
|
|
idtac "---------- plus_n_Sm ---------".
|
|
Print Assumptions plus_n_Sm.
|
|
idtac "---------- add_comm ---------".
|
|
Print Assumptions add_comm.
|
|
idtac "---------- add_assoc ---------".
|
|
Print Assumptions add_assoc.
|
|
idtac "---------- double_plus ---------".
|
|
Print Assumptions double_plus.
|
|
idtac "---------- eqb_refl ---------".
|
|
Print Assumptions eqb_refl.
|
|
idtac "---------- add_shuffle3 ---------".
|
|
Print Assumptions add_shuffle3.
|
|
idtac "---------- mul_comm ---------".
|
|
Print Assumptions mul_comm.
|
|
idtac "---------- bin_to_nat_pres_incr ---------".
|
|
Print Assumptions bin_to_nat_pres_incr.
|
|
idtac "---------- nat_bin_nat ---------".
|
|
Print Assumptions nat_bin_nat.
|
|
idtac "".
|
|
idtac "********** Advanced **********".
|
|
idtac "---------- double_incr ---------".
|
|
Print Assumptions double_incr.
|
|
idtac "---------- double_bin_zero ---------".
|
|
Print Assumptions double_bin_zero.
|
|
idtac "---------- double_incr_bin ---------".
|
|
Print Assumptions double_incr_bin.
|
|
idtac "---------- bin_nat_bin ---------".
|
|
Print Assumptions bin_nat_bin.
|
|
Abort.
|
|
|
|
(* 2026-01-07 13:18 *)
|
|
|
|
(* 2026-01-07 13:18 *)
|