TraceClassicalProperties.v

From Coq Require Import Classical ClassicalEpsilon.

[Loading ML file ring_plugin.cmxs (using legacy method) ... done]

From VLSM.Lib Require Import SsrExport Traces TraceProperties.

[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]

[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]

Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits.

Lemma not_infiniteT_finiteT : forall tr : trace, ~ infiniteT tr -> finiteT tr.

A, B: Type
forall tr : trace, ~ infiniteT tr -> finiteT tr

Proof.

A, B: Type
forall tr : trace, ~ infiniteT tr -> finiteT tr

move => tr Hnot.

A, B: Type
tr: trace
Hnot: ~ infiniteT tr
finiteT tr

case: (classic (finiteT tr)) => Hinf //.

A, B: Type
tr: trace
Hnot: ~ infiniteT tr
Hinf: ~ finiteT tr
finiteT tr

case: Hnot.

A, B: Type
tr: trace
Hinf: ~ finiteT tr
infiniteT tr

exact: not_finiteT_infiniteT. Qed. Lemma finiteT_infiniteT : forall tr : trace, finiteT tr \/ infiniteT tr.

A, B: Type
forall tr : trace, finiteT tr \/ infiniteT tr

Proof.

A, B: Type
forall tr : trace, finiteT tr \/ infiniteT tr

move => tr.

A, B: Type
tr: trace
finiteT tr \/ infiniteT tr

case: (classic (finiteT tr)) => Hinf; first by left.

A, B: Type
tr: trace
Hinf: ~ finiteT tr
finiteT tr \/ infiniteT tr

right; exact: not_finiteT_infiniteT. Qed. Definition finiteT_infiniteT_dec (tr : trace) : { finiteT tr }+{ infiniteT tr } := match excluded_middle_informative (finiteT tr) with | left Hfin => left Hfin | right Hfin => right (not_finiteT_infiniteT Hfin) end.

CoFixpoint midp (p0 p1 : trace -> Prop) tr0 tr1 (h : followsT (appendT p0 p1) tr0 tr1) : trace := match followsT_dec h with | inl (existT tr (exist a (conj _ (conj _ H)))) => let: exist x _ := constructive_indefinite_description _ H in x | inr (existT tr (existT tr' (existT a (exist b (conj _ (conj _ H)))))) => Tcons a b (@midp _ _ _ _ H) end. Lemma midpointT_midp : forall (p0 p1 : trace -> Prop) tr0 tr1 (h : followsT (appendT p0 p1) tr0 tr1), midpointT h (midp h).

A, B: Type
forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)

Proof.

A, B: Type
forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)

cofix CIH.

A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)
forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)

dependent inversion h; subst.

A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)
p0, p1: trace -> Prop
tr1: trace
h: followsT (p0 *+* p1) (Tnil (hd tr1)) tr1
a0: (p0 *+* p1) tr1
midpointT (followsT_nil eq_refl a0) (midp (followsT_nil eq_refl a0))

A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
midpointT (followsT_delay a b f) (midp (followsT_delay a b f))

A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)
p0, p1: trace -> Prop
tr1: trace
h: followsT (p0 *+* p1) (Tnil (hd tr1)) tr1
a0: (p0 *+* p1) tr1
midpointT (followsT_nil eq_refl a0) (midp (followsT_nil eq_refl a0))

A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
midpointT (followsT_delay a b f) (midp (followsT_delay a b f))

rewrite [midp _]trace_destr /=.

A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)
p0, p1: trace -> Prop
tr1: trace
h: followsT (p0 *+* p1) (Tnil (hd tr1)) tr1
a0: (p0 *+* p1) tr1
midpointT (followsT_nil eq_refl a0) match (let '@exist _ _ x _ := constructive_indefinite_description (fun tr' : trace => p0 tr' /\ followsT p1 tr' tr1) a0 in x) with | Tnil a => Tnil a | Tcons a b tr' => Tcons a b tr' end

A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
midpointT (followsT_delay a b f) (midp (followsT_delay a b f))

case: (constructive_indefinite_description _ _) => /= x [a1 hm].

A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)
p0, p1: trace -> Prop
tr1: trace
h: followsT (p0 *+* p1) (Tnil (hd tr1)) tr1
a0: (p0 *+* p1) tr1
x: trace
a1: p0 x
hm: followsT p1 x tr1
midpointT (followsT_nil eq_refl a0) match x with | Tnil a => Tnil a | Tcons a b tr' => Tcons a b tr' end

A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
midpointT (followsT_delay a b f) (midp (followsT_delay a b f))

by apply: midpointT_nil => //; case: x a1 hm.

A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
midpointT (followsT_delay a b f) (midp (followsT_delay a b f))

rewrite [midp _]trace_destr /=.

A, B: Type
CIH: forall (p0 p1 : trace -> Prop) (tr0 tr1 : trace) (h : followsT (p0 *+* p1) tr0 tr1), midpointT h (midp h)
p0, p1: trace -> Prop
a: A
b: B
tr, tr': trace
h: followsT (p0 *+* p1) (Tcons a b tr) (Tcons a b tr')
f: followsT (p0 *+* p1) tr tr'
midpointT (followsT_delay a b f) (Tcons a b (midp f))

exact: (@midpointT_delay _ _ p0 p1 (Tcons a b tr) (Tcons a b tr') (followsT_delay a b f) tr tr' f a b (midp f)). Qed. Lemma appendT_assoc_R : forall p1 p2 p3, forall tr : trace, (appendT p1 (appendT p2 p3)) tr -> (appendT (appendT p1 p2) p3) tr.

A, B: Type
forall (p1 p2 p3 : trace -> Prop) (tr : trace), (p1 *+* p2 *+* p3) tr -> ((p1 *+* p2) *+* p3) tr

Proof.

A, B: Type
forall (p1 p2 p3 : trace -> Prop) (tr : trace), (p1 *+* p2 *+* p3) tr -> ((p1 *+* p2) *+* p3) tr

move => p1 p2 p3 tr0 [tr1 [h1 h2]].

A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h1: p1 tr1
h2: followsT (p2 *+* p3) tr1 tr0
((p1 *+* p2) *+* p3) tr0

exists (midp h2); split.

A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h1: p1 tr1
h2: followsT (p2 *+* p3) tr1 tr0
(p1 *+* p2) (midp h2)

A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h1: p1 tr1
h2: followsT (p2 *+* p3) tr1 tr0
followsT p3 (midp h2) tr0

A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h1: p1 tr1
h2: followsT (p2 *+* p3) tr1 tr0
(p1 *+* p2) (midp h2)

A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h1: p1 tr1
h2: followsT (p2 *+* p3) tr1 tr0
followsT p3 (midp h2) tr0

exists tr1; split => //.

A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h1: p1 tr1
h2: followsT (p2 *+* p3) tr1 tr0
followsT p2 tr1 (midp h2)

A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h1: p1 tr1
h2: followsT (p2 *+* p3) tr1 tr0
followsT p3 (midp h2) tr0

exact: (midpointT_before (midpointT_midp h2)).

A, B: Type
p1, p2, p3: trace -> Prop
tr0, tr1: trace
h1: p1 tr1
h2: followsT (p2 *+* p3) tr1 tr0
followsT p3 (midp h2) tr0

exact: (midpointT_after (midpointT_midp h2)). Qed. Lemma AppendT_assoc_R : forall (p1 p2 p3 : propT), (p1 *** p2 *** p3) =>> (p1 *** p2) *** p3.

A, B: Type
forall p1 p2 p3 : propT, (p1 *** p2 *** p3) =>> (p1 *** p2) *** p3

Proof.

A, B: Type
forall p1 p2 p3 : propT, (p1 *** p2 *** p3) =>> (p1 *** p2) *** p3

move => [f1 hf1] [f2 hf2] [f3 hf3] tr0 /= h1.

A, B: Type
f1: trace -> Prop
hf1: setoidT f1
f2: trace -> Prop
hf2: setoidT f2
f3: trace -> Prop
hf3: setoidT f3
tr0: trace
h1: (f1 *+* f2 *+* f3) tr0
((f1 *+* f2) *+* f3) tr0

exact: appendT_assoc_R. Qed. End sec_trace_classical_properties.

Utility: Properties of Possibly-Infinite Traces Requiring Classical Logic

Relating finiteness and infiniteness

Using midpoints to show the right associativity of the append property