forked from oysteikt/sf1-template
276 lines
7.3 KiB
Coq
276 lines
7.3 KiB
Coq
Set Warnings "-notation-overridden,-parsing".
|
|
From Stdlib Require Export String.
|
|
From LF Require Import Tactics.
|
|
|
|
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 Tactics.
|
|
Import Check.
|
|
|
|
Goal True.
|
|
|
|
idtac "------------------- apply_exercise1 --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> rev_exercise1".
|
|
idtac "Possible points: 2".
|
|
check_type @rev_exercise1 (
|
|
(forall (l l' : list nat) (_ : @eq (list nat) l (@rev nat l')),
|
|
@eq (list nat) l' (@rev nat l))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions rev_exercise1.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- injection_ex3 --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> injection_ex3".
|
|
idtac "Possible points: 3".
|
|
check_type @injection_ex3 (
|
|
(forall (X : Type) (x y z : X) (l j : list X)
|
|
(_ : @eq (list X) (@cons X x (@cons X y l)) (@cons X z j))
|
|
(_ : @eq (list X) j (@cons X z l)),
|
|
@eq X x y)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions injection_ex3.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- discriminate_ex3 --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> discriminate_ex3".
|
|
idtac "Possible points: 1".
|
|
check_type @discriminate_ex3 (
|
|
(forall (X : Type) (x y z : X) (l _ : list X)
|
|
(_ : @eq (list X) (@cons X x (@cons X y l)) (@nil X)),
|
|
@eq X x z)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions discriminate_ex3.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- nth_error_always_none --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> nth_error_always_none".
|
|
idtac "Possible points: 3".
|
|
check_type @nth_error_always_none (
|
|
(forall (l : list nat)
|
|
(_ : forall i : nat, @eq (option nat) (@nth_error nat l i) (@None nat)),
|
|
@eq (list nat) l (@nil nat))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions nth_error_always_none.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- eqb_true --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> eqb_true".
|
|
idtac "Possible points: 2".
|
|
check_type @eqb_true ((forall (n m : nat) (_ : @eq bool (eqb n m) true), @eq nat n m)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions eqb_true.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- plus_n_n_injective --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> plus_n_n_injective".
|
|
idtac "Possible points: 3".
|
|
check_type @plus_n_n_injective (
|
|
(forall (n m : nat) (_ : @eq nat (Nat.add n n) (Nat.add m m)), @eq nat n m)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions plus_n_n_injective.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- gen_dep_practice --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> nth_error_after_last".
|
|
idtac "Possible points: 3".
|
|
check_type @nth_error_after_last (
|
|
(forall (n : nat) (X : Type) (l : list X) (_ : @eq nat (@length X l) n),
|
|
@eq (option X) (@nth_error X l n) (@None X))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions nth_error_after_last.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- combine_split --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> combine_split".
|
|
idtac "Possible points: 3".
|
|
check_type @combine_split (
|
|
(forall (X Y : Type) (l : list (prod X Y)) (l1 : list X)
|
|
(l2 : list Y)
|
|
(_ : @eq (prod (list X) (list Y)) (@split X Y l)
|
|
(@pair (list X) (list Y) l1 l2)),
|
|
@eq (list (prod X Y)) (@combine X Y l1 l2) l)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions combine_split.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- destruct_eqn_practice --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> bool_fn_applied_thrice".
|
|
idtac "Possible points: 2".
|
|
check_type @bool_fn_applied_thrice (
|
|
(forall (f : forall _ : bool, bool) (b : bool), @eq bool (f (f (f b))) (f b))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions bool_fn_applied_thrice.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- eqb_sym --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> eqb_sym".
|
|
idtac "Possible points: 3".
|
|
check_type @eqb_sym ((forall n m : nat, @eq bool (eqb n m) (eqb m n))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions eqb_sym.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- split_combine --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> Manually graded: split_combine".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 3".
|
|
print_manual_grade manual_grade_for_split_combine.
|
|
idtac " ".
|
|
|
|
idtac "------------------- filter_exercise --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> filter_exercise".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 3".
|
|
check_type @filter_exercise (
|
|
(forall (X : Type) (test : forall _ : X, bool) (x : X)
|
|
(l lf : list X) (_ : @eq (list X) (@filter X test l) (@cons X x lf)),
|
|
@eq bool (test x) true)).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions filter_exercise.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac "------------------- forall_exists_challenge --------------------".
|
|
idtac " ".
|
|
|
|
idtac "#> existsb_existsb'".
|
|
idtac "Advanced".
|
|
idtac "Possible points: 6".
|
|
check_type @existsb_existsb' (
|
|
(forall (X : Type) (test : forall _ : X, bool) (l : list X),
|
|
@eq bool (@existsb X test l) (@existsb' X test l))).
|
|
idtac "Assumptions:".
|
|
Abort.
|
|
Print Assumptions existsb_existsb'.
|
|
Goal True.
|
|
idtac " ".
|
|
|
|
idtac " ".
|
|
|
|
idtac "Max points - standard: 25".
|
|
idtac "Max points - advanced: 37".
|
|
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 "---------- rev_exercise1 ---------".
|
|
Print Assumptions rev_exercise1.
|
|
idtac "---------- injection_ex3 ---------".
|
|
Print Assumptions injection_ex3.
|
|
idtac "---------- discriminate_ex3 ---------".
|
|
Print Assumptions discriminate_ex3.
|
|
idtac "---------- nth_error_always_none ---------".
|
|
Print Assumptions nth_error_always_none.
|
|
idtac "---------- eqb_true ---------".
|
|
Print Assumptions eqb_true.
|
|
idtac "---------- plus_n_n_injective ---------".
|
|
Print Assumptions plus_n_n_injective.
|
|
idtac "---------- nth_error_after_last ---------".
|
|
Print Assumptions nth_error_after_last.
|
|
idtac "---------- combine_split ---------".
|
|
Print Assumptions combine_split.
|
|
idtac "---------- bool_fn_applied_thrice ---------".
|
|
Print Assumptions bool_fn_applied_thrice.
|
|
idtac "---------- eqb_sym ---------".
|
|
Print Assumptions eqb_sym.
|
|
idtac "".
|
|
idtac "********** Advanced **********".
|
|
idtac "---------- split_combine ---------".
|
|
idtac "MANUAL".
|
|
idtac "---------- filter_exercise ---------".
|
|
Print Assumptions filter_exercise.
|
|
idtac "---------- existsb_existsb' ---------".
|
|
Print Assumptions existsb_existsb'.
|
|
Abort.
|
|
|
|
(* 2026-01-07 13:18 *)
|
|
|
|
(* 2026-01-07 13:18 *)
|