|
Positive |
Negative |
|---|---|
Inductive finite : trace -> Prop :=
| Fin_Tnil : forall a, finite (Tnil a)
| Fin_Tcons : forall (a : A) (b : B) tr,
finite tr -> finite (Tcons a b tr).
Lemma invert_finite_Tcons (a : A) (b : B)
(tr : trace) (h : finite (Tcons a b tr))
: finite tr.
Proof. now inversion h. Defined.
Fixpoint final (tr : trace)
(h : finite tr) {struct h} : A :=
match tr as tr' return (finite tr' -> A) with
| Tnil a => fun _ => a
| Tcons a b tr0 =>
fun h => final (invert_finite_Tcons h)
end h. |
Inductive finite' : trace' -> Prop :=
| Fin_Tnil : forall a, finite' (TnilF a)
| Fin_Tcons : forall (a : A) (b : B) tr,
finite' (observe tr) -> finite' (TconsF a b tr).
Definition finite : trace -> Prop :=
fun tr => finite' (observe tr).
Lemma invert_finite'_Tcons (a : A) (b : B)
(tr : trace) (h : finite' (TconsF a b tr))
: finite' (observe tr).
Proof. now inversion h. Defined.
Definition final' : forall (tr: trace'),
finite' tr -> A :=
fix F (tr : trace')
(h : finite' tr) {struct h} : A :=
match tr as tr' return (finite' tr' -> A) with
| TnilF a => fun _ => a
| TconsF a b tr0 =>
fun h => F (observe tr0) (invert_finite'_Tcons h)
end h.
Definition final (tr : trace) (h : finite tr) : A :=
final' h. |
Last active
July 23, 2023 21:17
-
-
Save palmskog/d4e72d3d1424f34edf84f500f55e39ad to your computer and use it in GitHub Desktop.
Positive vs. negative coinductive finiteness in Coq
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment