hs-to-coq/examples/rle/Proofs.v at master · antalsz/hs-to-coq · GitHub

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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
Require Import Prelude.
Require Import RLE.

Require Import Proofs.GHC.Base.

(* This example uses the following lemma from the Base library theory:

     map_map

*)

Lemma group_by_not_nil:
  forall f (xs : list E),
    ~ In nil (groupBy f xs).
Proof.
  induction xs.
  * simpl. auto.
  * simpl.
    destruct (groupBy f xs) eqn:?.
    - simpl in *.
      intuition congruence.
    - destruct l eqn:?.
      + intuition.
      + destruct (f a e).
        ** contradict IHxs.
           destruct IHxs; try congruence.
           intuition.
        ** contradict IHxs.
           destruct IHxs; try congruence.
Qed.


Lemma concat_groupBy:
  forall f (xs : list E),
    concat (groupBy f xs) = xs.
Proof.
  intros.
  induction xs.
  * reflexivity.
  * simpl.
    destruct (groupBy f xs) eqn:?.
    - simpl in IHxs.  unfold concat in *. simpl in *. congruence.
    - destruct l eqn:?.
      + exfalso.
        apply (group_by_not_nil f xs).
        rewrite Heql.
        intuition.
      + destruct (f a e); unfold concat in *; simpl in *; congruence.
Qed.

(*
Lemma map_map:
  forall a b c (f : a -> b) (g : b -> c) (x : list a),
  map g (map f x) = map (g ∘ f) x.
Proof.
  intros.
  induction x.
  * auto.
  * simpl. rewrite IHx. auto.
Qed.

*)


Lemma in_map_hd_in_concat:
  forall (x : E) xs,
  ~ In nil xs ->
  In x (map hd xs) ->
  In x (concat xs).
Proof.
  intros.
  induction xs.
  * inversion H0.
  * simpl.
    unfold concat. simpl.
    rewrite in_app_iff.
    destruct H0.
    - left.
      subst.
      destruct a.
      + contradict H. intuition.
      + intuition.
    - right.
      apply IHxs.
      + contradict H. right. assumption.
      + assumption.
Qed.

(* For the good rle, we can prove
   properties about it, simply because we
   never look at the axiom. *)
Lemma rle_dom:
  forall `{Eq_ E} (x : E) xs,
    In x (map fst (rle xs)) -> In x xs.
Proof.
  intros.
  unfold rle in H0.
  rewrite map_map in H0.
  apply in_map_hd_in_concat in H0.
  unfold group in H0.
  rewrite concat_groupBy in H0.
  assumption.
  apply group_by_not_nil.
Qed.


(* For the bad rle, at some point we
   would have to prove that [hd nil] is in [xs].
   We would not be able to prove that in general. *)
Lemma int_suc_absurd: forall x : Int,  (#1 + x <> x).
Proof.
  intros.
  change ((1 + x)%Z <> (0 + x)%Z).
  rewrite Z.add_cancel_r.
  destruct (Z.eq_dec 1 0); intuition congruence.
Qed.

Lemma bad_rle_dom:
  exists (x : Int) xs,
    In x (map fst (bad_rle xs)) /\ ~ (In x xs).
Proof.
  remember (hd nil : Int) as x.
  exists x.
  exists (cons (#1 + x) nil).
  split.
  * left. subst. reflexivity.
  * intro.
    destruct H.
    - apply (int_suc_absurd _ H).
    - destruct H.
Qed.