palmskog

Positive vs. negative coinductive finiteness in Coq

Positive

palmskog

From Coq Require Import RelationClasses Program.Basics.
From Coinduction Require Import all.
Import CoindNotations.
Lemma gfp_leq_Chain {X} {L : CompleteLattice X} (b : mon X) (R : Chain b) :
  gfp b <= b ` R.
Proof.
  rewrite <- (gfp_fp b).
  apply b.
  eapply gfp_chain.
Qed.

palmskog

From Cdcl Require Import Itauto.
From stdpp Require Import prelude.

Inductive Sorted : list nat -> Prop :=
| sorted_nil : Sorted []
| sorted_singleton : forall n, Sorted [n]
| sorted_cons : forall n m p, n <= m -> Sorted (m :: p) -> Sorted (n :: m :: p).

#[local] Hint Constructors Sorted : core.

palmskog

(* generated by Ott 0.32 from: regexp.ott *)

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import Ott.ott_list_core.


Import ListNotations.
Section RegExp.

palmskog

From Coq Require Import Arith Lia.

Lemma monotonic_inverse :
 forall f : nat -> nat,
 (forall x y : nat, x < y -> f x < f y) ->
 forall x y : nat, f x < f y -> x < y.
Proof.
intros f Hmon x y Hlt; case (le_gt_dec y x); auto.
intros Hle; elim (le_lt_or_eq _ _ Hle).
intros Hlt'; elim (lt_asym _ _ Hlt); apply Hmon; auto.

palmskog

Require Import Arith.
Require Import Bool.
Require Import List.


Definition n : Set := nat.
Definition k : Set := nat.

Inductive Label : Set := 
 | Receive : Label

palmskog

Require Import List.
Require Import Sorting.Permutation.
Require Import Arith.
Require Import Wf_nat.
Require Import ssreflect.

Section Alternate.

Variable A : Type.

palmskog

(** SSReflect boilerplate. *)
From Coq Require Import ssreflect.
Set SsrOldRewriteGoalsOrder.
Set Asymmetric Patterns.
Set Bullet Behavior "None".
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

(** Traces as lazy lists of booleans. *)

palmskog

(** SSReflect boilerplate. *)
From Coq Require Import ssreflect.
Set SsrOldRewriteGoalsOrder.
Set Asymmetric Patterns.
Set Bullet Behavior "None".
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

(** Traces as lazy lists of booleans. *)

palmskog

type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

type ('a, 'b) sum =
| Inl of 'a
| Inr of 'b

(** val fst : ('a1 * 'a2) -> 'a1 **)