forked from oysteikt/sf1-template
545 lines
15 KiB
Coq
545 lines
15 KiB
Coq
Set Warnings "-notation-overridden,-parsing".
|
|
From Stdlib Require Export String.
|
|
From LF Require Import Lists.
|
|
|
|
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 Lists.
|
|
Import Check.
|
|
|
|
Goal True.
|
|
|
|
idtac "------------------- snd_fst_is_swap --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.snd_fst_is_swap".
|
|
idtac "Possible points: 1".
|
|
check_type @NatList.snd_fst_is_swap (
|
|
(forall p : NatList.natprod,
|
|
@eq NatList.natprod (NatList.pair (NatList.snd p) (NatList.fst p))
|
|
(NatList.swap_pair p))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.snd_fst_is_swap.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- list_funs --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_nonzeros".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.test_nonzeros (
|
|
(@eq NatList.natlist
|
|
(NatList.nonzeros
|
|
(NatList.cons 0
|
|
(NatList.cons 1
|
|
(NatList.cons 0
|
|
(NatList.cons 2
|
|
(NatList.cons 3
|
|
(NatList.cons 0 (NatList.cons 0 NatList.nil))))))))
|
|
(NatList.cons 1 (NatList.cons 2 (NatList.cons 3 NatList.nil))))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_nonzeros.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_oddmembers".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.test_oddmembers (
|
|
(@eq NatList.natlist
|
|
(NatList.oddmembers
|
|
(NatList.cons 0
|
|
(NatList.cons 1
|
|
(NatList.cons 0
|
|
(NatList.cons 2
|
|
(NatList.cons 3
|
|
(NatList.cons 0 (NatList.cons 0 NatList.nil))))))))
|
|
(NatList.cons 1 (NatList.cons 3 NatList.nil)))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_oddmembers.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_countoddmembers2".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.test_countoddmembers2 (
|
|
(@eq nat
|
|
(NatList.countoddmembers
|
|
(NatList.cons 0 (NatList.cons 2 (NatList.cons 4 NatList.nil))))
|
|
0)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_countoddmembers2.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_countoddmembers3".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.test_countoddmembers3 (
|
|
(@eq nat (NatList.countoddmembers NatList.nil) 0)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_countoddmembers3.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- alternate --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_alternate1".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 1".
|
|
check_type @NatList.test_alternate1 (
|
|
(@eq NatList.natlist
|
|
(NatList.alternate
|
|
(NatList.cons 1 (NatList.cons 2 (NatList.cons 3 NatList.nil)))
|
|
(NatList.cons 4 (NatList.cons 5 (NatList.cons 6 NatList.nil))))
|
|
(NatList.cons 1
|
|
(NatList.cons 4
|
|
(NatList.cons 2
|
|
(NatList.cons 5 (NatList.cons 3 (NatList.cons 6 NatList.nil)))))))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_alternate1.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_alternate2".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 1".
|
|
check_type @NatList.test_alternate2 (
|
|
(@eq NatList.natlist
|
|
(NatList.alternate (NatList.cons 1 NatList.nil)
|
|
(NatList.cons 4 (NatList.cons 5 (NatList.cons 6 NatList.nil))))
|
|
(NatList.cons 1
|
|
(NatList.cons 4 (NatList.cons 5 (NatList.cons 6 NatList.nil)))))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_alternate2.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_alternate4".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 1".
|
|
check_type @NatList.test_alternate4 (
|
|
(@eq NatList.natlist
|
|
(NatList.alternate NatList.nil
|
|
(NatList.cons 20 (NatList.cons 30 NatList.nil)))
|
|
(NatList.cons 20 (NatList.cons 30 NatList.nil)))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_alternate4.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- bag_functions --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_count2".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.test_count2 (
|
|
(@eq nat
|
|
(NatList.count 6
|
|
(NatList.cons 1
|
|
(NatList.cons 2
|
|
(NatList.cons 3
|
|
(NatList.cons 1 (NatList.cons 4 (NatList.cons 1 NatList.nil)))))))
|
|
0)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_count2.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_sum1".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.test_sum1 (
|
|
(@eq nat
|
|
(NatList.count 1
|
|
(NatList.sum
|
|
(NatList.cons 1 (NatList.cons 2 (NatList.cons 3 NatList.nil)))
|
|
(NatList.cons 1 (NatList.cons 4 (NatList.cons 1 NatList.nil)))))
|
|
3)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_sum1.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_add1".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.test_add1 (
|
|
(@eq nat
|
|
(NatList.count 1
|
|
(NatList.add 1
|
|
(NatList.cons 1 (NatList.cons 4 (NatList.cons 1 NatList.nil)))))
|
|
3)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_add1.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_add2".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.test_add2 (
|
|
(@eq nat
|
|
(NatList.count 5
|
|
(NatList.add 1
|
|
(NatList.cons 1 (NatList.cons 4 (NatList.cons 1 NatList.nil)))))
|
|
0)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_add2.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_member1".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.test_member1 (
|
|
(@eq bool
|
|
(NatList.member 1
|
|
(NatList.cons 1 (NatList.cons 4 (NatList.cons 1 NatList.nil))))
|
|
true)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_member1.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_member2".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.test_member2 (
|
|
(@eq bool
|
|
(NatList.member 2
|
|
(NatList.cons 1 (NatList.cons 4 (NatList.cons 1 NatList.nil))))
|
|
false)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_member2.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- list_exercises --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.app_nil_r".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.app_nil_r (
|
|
(forall l : NatList.natlist,
|
|
@eq NatList.natlist (NatList.app l NatList.nil) l)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.app_nil_r.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.rev_app_distr".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.rev_app_distr (
|
|
(forall l1 l2 : NatList.natlist,
|
|
@eq NatList.natlist (NatList.rev (NatList.app l1 l2))
|
|
(NatList.app (NatList.rev l2) (NatList.rev l1)))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.rev_app_distr.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.rev_involutive".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.rev_involutive (
|
|
(forall l : NatList.natlist,
|
|
@eq NatList.natlist (NatList.rev (NatList.rev l)) l)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.rev_involutive.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.app_assoc4".
|
|
idtac "Possible points: 0.5".
|
|
check_type @NatList.app_assoc4 (
|
|
(forall l1 l2 l3 l4 : NatList.natlist,
|
|
@eq NatList.natlist (NatList.app l1 (NatList.app l2 (NatList.app l3 l4)))
|
|
(NatList.app (NatList.app (NatList.app l1 l2) l3) l4))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.app_assoc4.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.nonzeros_app".
|
|
idtac "Possible points: 1".
|
|
check_type @NatList.nonzeros_app (
|
|
(forall l1 l2 : NatList.natlist,
|
|
@eq NatList.natlist (NatList.nonzeros (NatList.app l1 l2))
|
|
(NatList.app (NatList.nonzeros l1) (NatList.nonzeros l2)))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.nonzeros_app.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- eqblist --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.eqblist_refl".
|
|
idtac "Possible points: 2".
|
|
check_type @NatList.eqblist_refl (
|
|
(forall l : NatList.natlist, @eq bool true (NatList.eqblist l l))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.eqblist_refl.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- count_member_nonzero --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.count_member_nonzero".
|
|
idtac "Possible points: 1".
|
|
check_type @NatList.count_member_nonzero (
|
|
(forall s : NatList.bag,
|
|
@eq bool (leb 1 (NatList.count 1 (NatList.cons 1 s))) true)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.count_member_nonzero.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- remove_does_not_increase_count --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.remove_does_not_increase_count".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 3".
|
|
check_type @NatList.remove_does_not_increase_count (
|
|
(forall s : NatList.bag,
|
|
@eq bool
|
|
(leb (NatList.count 0 (NatList.remove_one 0 s)) (NatList.count 0 s)) true)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.remove_does_not_increase_count.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- involution_injective --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.involution_injective".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 3".
|
|
check_type @NatList.involution_injective (
|
|
(forall (f : forall _ : nat, nat) (_ : forall n : nat, @eq nat n (f (f n)))
|
|
(n1 n2 : nat) (_ : @eq nat (f n1) (f n2)),
|
|
@eq nat n1 n2)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.involution_injective.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- rev_injective --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.rev_injective".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 2".
|
|
check_type @NatList.rev_injective (
|
|
(forall (l1 l2 : NatList.natlist)
|
|
(_ : @eq NatList.natlist (NatList.rev l1) (NatList.rev l2)),
|
|
@eq NatList.natlist l1 l2)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.rev_injective.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- hd_error --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_hd_error1".
|
|
idtac "Possible points: 1".
|
|
check_type @NatList.test_hd_error1 (
|
|
(@eq NatList.natoption (NatList.hd_error NatList.nil) NatList.None)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_hd_error1.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "#> NatList.test_hd_error2".
|
|
idtac "Possible points: 1".
|
|
check_type @NatList.test_hd_error2 (
|
|
(@eq NatList.natoption (NatList.hd_error (NatList.cons 1 NatList.nil))
|
|
(NatList.Some 1))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions NatList.test_hd_error2.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- eqb_id_refl --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> eqb_id_refl".
|
|
idtac "Possible points: 1".
|
|
check_type @eqb_id_refl ((forall x : id, @eq bool (eqb_id x x) true)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions eqb_id_refl.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- update_eq --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> PartialMap.update_eq".
|
|
idtac "Possible points: 1".
|
|
check_type @PartialMap.update_eq (
|
|
(forall (d : PartialMap.partial_map) (x : id) (v : nat),
|
|
@eq NatList.natoption (PartialMap.find x (PartialMap.update d x v))
|
|
(NatList.Some v))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions PartialMap.update_eq.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- update_neq --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> PartialMap.update_neq".
|
|
idtac "Possible points: 1".
|
|
check_type @PartialMap.update_neq (
|
|
(forall (d : PartialMap.partial_map) (x y : id) (o : nat)
|
|
(_ : @eq bool (eqb_id x y) false),
|
|
@eq NatList.natoption (PartialMap.find x (PartialMap.update d y o))
|
|
(PartialMap.find x d))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions PartialMap.update_neq.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac " ".
|
|
|
|
idtac "Max points - standard: 17".
|
|
idtac "Max points - advanced: 28".
|
|
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 "---------- NatList.snd_fst_is_swap ---------".
|
|
Print Assumptions NatList.snd_fst_is_swap.
|
|
idtac "---------- NatList.test_nonzeros ---------".
|
|
Print Assumptions NatList.test_nonzeros.
|
|
idtac "---------- NatList.test_oddmembers ---------".
|
|
Print Assumptions NatList.test_oddmembers.
|
|
idtac "---------- NatList.test_countoddmembers2 ---------".
|
|
Print Assumptions NatList.test_countoddmembers2.
|
|
idtac "---------- NatList.test_countoddmembers3 ---------".
|
|
Print Assumptions NatList.test_countoddmembers3.
|
|
idtac "---------- NatList.test_count2 ---------".
|
|
Print Assumptions NatList.test_count2.
|
|
idtac "---------- NatList.test_sum1 ---------".
|
|
Print Assumptions NatList.test_sum1.
|
|
idtac "---------- NatList.test_add1 ---------".
|
|
Print Assumptions NatList.test_add1.
|
|
idtac "---------- NatList.test_add2 ---------".
|
|
Print Assumptions NatList.test_add2.
|
|
idtac "---------- NatList.test_member1 ---------".
|
|
Print Assumptions NatList.test_member1.
|
|
idtac "---------- NatList.test_member2 ---------".
|
|
Print Assumptions NatList.test_member2.
|
|
idtac "---------- NatList.app_nil_r ---------".
|
|
Print Assumptions NatList.app_nil_r.
|
|
idtac "---------- NatList.rev_app_distr ---------".
|
|
Print Assumptions NatList.rev_app_distr.
|
|
idtac "---------- NatList.rev_involutive ---------".
|
|
Print Assumptions NatList.rev_involutive.
|
|
idtac "---------- NatList.app_assoc4 ---------".
|
|
Print Assumptions NatList.app_assoc4.
|
|
idtac "---------- NatList.nonzeros_app ---------".
|
|
Print Assumptions NatList.nonzeros_app.
|
|
idtac "---------- NatList.eqblist_refl ---------".
|
|
Print Assumptions NatList.eqblist_refl.
|
|
idtac "---------- NatList.count_member_nonzero ---------".
|
|
Print Assumptions NatList.count_member_nonzero.
|
|
idtac "---------- NatList.test_hd_error1 ---------".
|
|
Print Assumptions NatList.test_hd_error1.
|
|
idtac "---------- NatList.test_hd_error2 ---------".
|
|
Print Assumptions NatList.test_hd_error2.
|
|
idtac "---------- eqb_id_refl ---------".
|
|
Print Assumptions eqb_id_refl.
|
|
idtac "---------- PartialMap.update_eq ---------".
|
|
Print Assumptions PartialMap.update_eq.
|
|
idtac "---------- PartialMap.update_neq ---------".
|
|
Print Assumptions PartialMap.update_neq.
|
|
idtac "".
|
|
idtac "********** Advanced **********".
|
|
idtac "---------- NatList.test_alternate1 ---------".
|
|
Print Assumptions NatList.test_alternate1.
|
|
idtac "---------- NatList.test_alternate2 ---------".
|
|
Print Assumptions NatList.test_alternate2.
|
|
idtac "---------- NatList.test_alternate4 ---------".
|
|
Print Assumptions NatList.test_alternate4.
|
|
idtac "---------- NatList.remove_does_not_increase_count ---------".
|
|
Print Assumptions NatList.remove_does_not_increase_count.
|
|
idtac "---------- NatList.involution_injective ---------".
|
|
Print Assumptions NatList.involution_injective.
|
|
idtac "---------- NatList.rev_injective ---------".
|
|
Print Assumptions NatList.rev_injective.
|
|
Abort.
|
|
|
|
(* 2026-01-07 13:18 *)
|
|
|
|
(* 2026-01-07 13:18 *)
|