-
Notifications
You must be signed in to change notification settings - Fork 2
/
SelectionTest.v
105 lines (87 loc) · 2.47 KB
/
SelectionTest.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
Set Warnings "-notation-overridden,-parsing".
From Coq Require Export String.
From VFA Require Import Selection.
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 (pair ?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 VFA Require Import Selection.
Import Check.
Goal True.
idtac "------------------- select_perm --------------------".
idtac " ".
idtac "#> select_perm".
idtac "Possible points: 3".
check_type @select_perm (
(forall (x : nat) (l : list nat),
let (y, r) := select x l in @Permutation.Permutation nat (x :: l) (y :: r))).
idtac "Assumptions:".
Abort.
Print Assumptions select_perm.
Goal True.
idtac " ".
idtac "------------------- selection_sort_perm --------------------".
idtac " ".
idtac "#> selection_sort_perm".
idtac "Possible points: 3".
check_type @selection_sort_perm (
(forall l : list nat, @Permutation.Permutation nat l (selection_sort l))).
idtac "Assumptions:".
Abort.
Print Assumptions selection_sort_perm.
Goal True.
idtac " ".
idtac "------------------- select_smallest --------------------".
idtac " ".
idtac "#> select_smallest".
idtac "Possible points: 3".
check_type @select_smallest (
(forall (x : nat) (al : list nat) (y : nat) (bl : list nat),
select x al = (y, bl) -> @Forall nat (fun z : nat => y <= z) bl)).
idtac "Assumptions:".
Abort.
Print Assumptions select_smallest.
Goal True.
idtac " ".
idtac "------------------- selection_sort_sorted --------------------".
idtac " ".
idtac "#> selection_sort_sorted".
idtac "Possible points: 3".
check_type @selection_sort_sorted ((forall al : list nat, sorted (selection_sort al))).
idtac "Assumptions:".
Abort.
Print Assumptions selection_sort_sorted.
Goal True.
idtac " ".
idtac "------------------- selsort'_perm --------------------".
idtac " ".
idtac "#> selsort'_perm".
idtac "Possible points: 3".
check_type @selsort'_perm (
(forall (n : nat) (l : list nat),
@length nat l = n -> @Permutation.Permutation nat l (selsort' l))).
idtac "Assumptions:".
Abort.
Print Assumptions selsort'_perm.
Goal True.
idtac " ".
idtac " ".
idtac "Max points - standard: 15".
idtac "Max points - advanced: 15".
Abort.