-
Notifications
You must be signed in to change notification settings - Fork 5
/
leads_to.v
78 lines (66 loc) · 3.18 KB
/
leads_to.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
(****************************************************************************)
(* *)
(* *)
(* Solange Coupet-Grimal *)
(* *)
(* *)
(* Laboratoire d'Informatique Fondamentale de Marseille *)
(* CMI-Technopole de Chateau-Gombert *)
(* 39, Rue F. Joliot Curie *)
(* 13453 MARSEILLE Cedex 13 *)
(* [email protected] *)
(* *)
(* *)
(* Coq V7.0 *)
(* Juillet 2002 *)
(* *)
(****************************************************************************)
(* leads_to.v *)
(****************************************************************************)
Require Export ltl.
Section leads_to.
Variable state label : Set.
Notation Stream := (stream state) (only parsing).
Notation Stream_formula := (stream_formula state) (only parsing).
(****************************************************************************)
Lemma trans_until_leads :
forall (A B C D E : stream_formula state) (str : stream state),
(A str -> until B C str) ->
leads_to_via C D E str ->
A str -> until (fun str : stream state => B str \/ D str) E str.
intros A B C D E str H_until H_always H_A.
generalize H_always; clear H_always.
unfold leads_to_via in |- *; unfold implies in |- *.
elim (H_until H_A); clear H_until H_A str.
intros str H_C H_always; inversion H_always.
rewrite H1 in H; rewrite H1.
elim (H H_C); clear H H0 H1 s0 str0 H_always H_C str.
intros str E_str; constructor 1; assumption.
intros s str D_str until_D_E until_or; constructor 2; auto.
intros s str B_str until_B_C H_always_until H_always; constructor 2; auto.
apply H_always_until; inversion H_always; assumption.
Qed.
Hint Resolve trans_until_leads : core.
Lemma trans_leads_to :
forall (A B C D E : stream_formula state) (str : stream state),
leads_to_via A B C str ->
leads_to_via C D E str ->
leads_to_via (fun str : stream state => A str \/ C str)
(fun str : stream state => B str \/ D str) E str.
intros A B C D E; cofix trans_leads_to.
intro str; case str; clear str.
intros s str H1 H2; constructor.
intro H; elim H; clear H.
inversion_clear H1.
intro H_A; eauto.
inversion_clear H2.
intro H_C.
elim (H H_C); clear H.
constructor 1; auto.
constructor 2; auto.
unfold leads_to_via in trans_leads_to; unfold implies in trans_leads_to.
apply trans_leads_to.
inversion H1; assumption.
inversion H2; assumption.
Qed.
End leads_to.