-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathaborted_proofs.txt
60 lines (59 loc) · 2.53 KB
/
aborted_proofs.txt
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
aaaaaaaaaaaTheorem remove_first_inverse_of_add_row_on_headed_empty_table : forall (r: row) (h: header) ,
remove_first_row_from_table r (add_row r (add_header h empty_table)) = (add_header h empty_table).
Proof.
intros r h.
simpl. induction r.
- simpl. destruct (Datatypes.length h =? 0) eqn:Heq.
+ simpl. reflexivity.
+ simpl. reflexivity.
- simpl. destruct a.
-- simpl. destruct (string_dec s s). simpl. destruct (row_eqb r r).
+ simpl. destruct (Datatypes.length h =? S (Datatypes.length r)) eqn:Heq.
++ simpl. destruct (string_dec s s). simpl. destruct (row_eqb r r). reflexivity.
reflexivity. simpl. reflexivity.
++ simpl. reflexivity.
+ destruct (Datatypes.length h =? S (Datatypes.length r)) eqn:Heq. simpl.
destruct (string_dec s s). simpl. destruct (row_eqb r r). reflexivity. reflexivity.
simpl. reflexivity. simpl. reflexivity.
+ destruct n. reflexivity.
-- simpl. induction n.
+ simpl. destruct (Datatypes.length h =? S (Datatypes.length r)) eqn:Heq. simpl.
destruct (row_eqb r r). simpl. reflexivity. reflexivity. simpl. reflexivity.
+simpl. destruct (Datatypes.length h =? S (Datatypes.length r)) eqn:Heq. simpl.
rewrite Nat.eqb_refl. simpl. destruct (row_eqb r r). reflexivity.
reflexivity. simpl. reflexivity.
-- destruct (Datatypes.length h =? S (Datatypes.length r)) eqn:Heq. simpl. reflexivity.
simpl. reflexivity.
Qed.
(** The false filter is like 0 if filtering is mulitplication *)
Lemma name_this : forall (r : row) (h: header) (col_ident : string) (a: entry) (f: entry -> bool),
f = (fun e => false) -> filter_row_by_entry f col_ident h (a::r) = filter_row_by_entry f col_ident h r.
Proof.
intros r h col_ident a f H_f.
induction r.
+induction h.
-simpl. reflexivity.
-simpl. destruct (string_dec col_ident a0) eqn:H_eq.
-- rewrite H_f. reflexivity.
-- induction h.
--- reflexivity.
--- reflexivity.
+ induction h.
- simpl. reflexivity.
- simpl. destruct (string_dec col_ident a1) eqn: Heq.
-- rewrite H_f. reflexivity.
Abort.
Theorem filter_property_of_false_filter_on_rows : forall (r : row) (h: header) (col_ident : string) (f: entry -> bool),
f = (fun e => false) -> filter_row_by_entry f col_ident h r = false.
Proof.
intros r h col_ident f H.
induction h.
+ induction r.
-reflexivity.
-reflexivity.
+ destruct (string_dec col_ident a) eqn:Heq.
- destruct r. reflexivity. simpl. rewrite Heq. rewrite H. reflexivity.
- induction r.
-- reflexivity.
-- simpl. rewrite Heq.
Abort.