coinduction/examples/tutorial.v at master · lukaszcz/coinduction · 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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
From Coinduction Require Import Coinduction.
From Hammer Require Import Tactics.

Open Scope type_scope.

CoInductive term : Set :=
| C : nat -> term
| A : term -> term
| B : term -> term -> term.

CoInductive Eq : term -> term -> Set :=
| eq_C : forall i, Eq (C i) (C i)
| eq_A : forall t t', Eq t t' -> Eq (A t) (A t')
| eq_B : forall s s' t t', Eq s s' -> Eq t t' -> Eq (B s t) (B s t').

Notation "A == B" := (Eq A B) (at level 70).

CoInduction lem_eq_refl : forall t, t == t.
Proof.
  cauto.
Qed.

CoInduction lem_eq_sym : forall s t, s == t -> t == s.
Proof.
  intros.
  generalize (CH t s); intro.
  destruct t.
  Show Proof.
  (* The proof does not satisfy the "weak case restriction" and our
  translation will fail. The problem is forward reasoning with the
  coinductive hypothesis, followed by destructing a term which was
  used as an argument to the coinductive hypothesis. *)

  Restart.

  intros; destruct t; destruct s; inversion_clear H; econstructor; eauto.

  Restart.

  cauto.
Qed.

CoInduction lem_eq_trans : forall t1 t2 t3, t1 == t2 -> t2 == t3 -> t1 == t3.
Proof.
  cauto.
Qed.

CoInductive Red : term -> term -> Set :=
| red_C : forall i, Red (C i) (C i)
| red_A : forall t t', Red t t' -> Red (A t) (A t')
| red_B : forall s s' t t', Red s s' -> Red t t' -> Red (B s t) (B s' t')
| red_AB : forall t t1 t2, Red t t1 -> Red t t2 -> Red (A t) (B t1 t2).

Notation "A ==> B" := (Red A B) (at level 70).

CoInduction lem_red_refl : forall t, t ==> t.
Proof.
  cauto.
Qed.

CoInduction lem_eq_to_red : forall t1 t2, t1 == t2 -> t1 ==> t2.
Proof.
  cauto using lem_eq_refl.
Qed.

CoInduction lem_red_trans : forall t1 t2 t3, t1 ==> t2 -> t2 ==> t3 -> t1 ==> t3.
Proof.
  intros t1 t2 t3 H1 H2.
  destruct H1; inversion_clear H2; econstructor; eauto.
  (* "cauto" can prove this in 1.7s *)
Qed.

CoInduction lem_red_ex : forall t, { s & t ==> s }.
Proof.
  intro t; destruct t; cauto using lem_red_refl.
Qed.

CoInductive Peak : term -> term -> term -> Set :=
| peak_C : forall i, Peak (C i) (C i) (C i)
| peak_A : forall s t t', Peak s t t' -> Peak (A s) (A t) (A t')
| peak_B : forall s t s1 t1 s2 t2, Peak s s1 s2 -> Peak t t1 t2 -> Peak (B s t) (B s1 t1) (B s2 t2)
| peak_AAB : forall s s' t1 t2, Peak s s' t1 -> Peak s s' t2 -> Peak (A s) (A s') (B t1 t2)
| peak_ABA : forall s s' t1 t2, Peak s t1 s' -> Peak s t2 s' -> Peak (A s) (B t1 t2) (A s')
| peak_ABB : forall s s1 s2 t1 t2, Peak s s1 t1 -> Peak s s2 t2 -> Peak (A s) (B s1 s2) (B t1 t2).

CoInduction lem_peak : forall s t t', s ==> t -> s ==> t' -> Peak s t t'.
Proof.
  destruct 1; inversion_clear 1; constructor; eauto.
Qed.

CoInduction lem_peak_rev : forall s t t', Peak s t t' -> (s ==> t) * (s ==> t').
Proof.
  intros s t t' H.
  inversion_clear H.
  - cauto.
  - cauto.
  - generalize (CH s0 s1 s2 H0); intro.
    generalize (CH t0 t1 t2 H1); intro.
    cauto.
  - generalize (CH s0 s' t1 H0); intro.
    generalize (CH s0 s' t2 H1); intro.
    cauto.
  - generalize (CH s0 t1 s' H0); intro.
    generalize (CH s0 t2 s' H1); intro.
    cauto.
  - generalize (CH s0 s1 t1 H0); intro.
    generalize (CH s0 s2 t2 H1); intro.
    cauto.
Qed.

CoInduction lem_confl : forall s t t', Peak s t t' -> { s' & (t ==> s') * (t' ==> s') }.
Proof.
  intros s t t' H.
  inversion_clear H.
  - cauto.
  - cauto.
  - generalize (CH s0 s1 s2 H0); generalize (CH t0 t1 t2 H1); intros.
    simp_hyps; eexists; split; constructor; eauto.
  - generalize (CH s0 s' t1 H0); intro.
    generalize (CH s0 s' t2 H1); intro.
    simp_hyps.
    exists (B__g term__r s'1 s'0).
    split; constructor; eauto.
  - generalize (CH s0 t1 s' H0); intro.
    generalize (CH s0 t2 s' H1); intro.
    simp_hyps; eexists; split; constructor; eauto.
  - generalize (CH s0 s1 t1 H0); intro.
    generalize (CH s0 s2 t2 H1); intro.
    simp_hyps; eexists; split; constructor; eauto.
Qed.

Corollary cor_confl : forall s t t', s ==> t -> s ==> t' -> { s' & (t ==> s') * (t' ==> s') }.
Proof.
  eauto using lem_confl, lem_peak.
Qed.

CoInductive Red0 : term -> term -> Prop :=
| red0_C : forall i, Red0 (C i) (C i)
| red0_A : forall t t', Red0 t t' -> Red0 (A t) (A t')
| red0_B : forall s s' t t', Red0 s s' -> Red0 t t' -> Red0 (B s t) (B s' t')
| red0_AB : forall t t1 t2, Red0 t t1 -> Red0 t t2 -> Red0 (A t) (B t1 t2).

Notation "A --> B" := (Red0 A B) (at level 70).

CoInduction lem_red0_refl : forall t, t --> t.
Proof.
  cauto.
Qed.