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

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

module Util {

  datatype Option<T> = Some(v:T) | None

  function unionMap<U(!new), V>(m: map<U,V>, m': map<U,V>): map<U,V>
    requires m !! m'; // disjoint
    ensures forall i :: i in unionMap(m, m') <==> i in m || i in m';
    ensures forall i :: i in m ==> unionMap(m, m')[i] == m[i];
    ensures forall i :: i in m' ==> unionMap(m, m')[i] == m'[i];
  {

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

fun  valid_derivation_deriv_premise_cake v2 = 
    (fn  v1 => List.member v1 v2);

   datatype fitch_prop =  Prop_cont
  |  Prop_imp (fitch_prop) (fitch_prop)
  |  Prop_or (fitch_prop) (fitch_prop)
  |  Prop_and (fitch_prop) (fitch_prop)
  |  Prop_neg (fitch_prop)
  |  Prop_p (char list);

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.