palmskog

Require Import Arith.

Fixpoint fin_of_nat (m n : nat) : fin n + {m >= n} :=
  match n with
    | 0 => inright (Nat.le_0_l _)
    | S n' =>
      match m with
        | 0 => inleft None
        | S m' =>
          match fin_of_nat m' n' with

palmskog

Fixpoint fin_of_nat (m n : nat) : fin n + {p | m = n + p} :=
  match n with
    | 0 => inr (exist _ m eq_refl)  
    | S n' =>
      match m with
        | 0 => inl None
        | S m' =>
          match fin_of_nat m' n' with
            | inl f => inl (Some f) 
            | inr (exist _ x H) => inr (exist _ x (f_equal _ H))

palmskog

diff --git a/exteq.v b/exteq.v
index a8fdd78..4a771bc 100644
--- a/exteq.v
+++ b/exteq.v
@@ -31,13 +31,13 @@ cofix cf. destruct 1. constructor. apply cf. assumption.
 Qed.
 
 Lemma exteq_trans :
-   forall s1 s2 s3, exteq s1 s2 -> exteq s2 s3 -> exteq s1 s3.
+   forall s1 s2 s3, exteq s2 s3 -> exteq s1 s2 -> exteq s1 s3.

palmskog

My encoding of liveness properties of distributed systems in Verdi primarily uses three sources of previous work:

• The treatment of fairness in actor systems by Agha et al. [1].
• Coq's mechanisms for coinductive predicates and corecursive functions, originally by Eduardo Gimenez [2].
• Verification of self-stabilizing population protocols in Coq by Deng and Monin [3].

Agha et al. define an operational semantics of actor systems, where the reduction rules are parameterized on certain variables (e.g., the name of the actor involved). They then define executions of actor systems as infinite sequences of system configurations, with each transition labeled with the name of the reduction rule applied, along with the arguments used as parameters. This allows them to consider only fair executions starting from some initial configuration.

A label is said to be enabled at some point in an execution if it is possible to make valid transition using the label to some new configuration. Intuitively, in the work

palmskog

opam init
eval $(opam config env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra ounit uuidm

git clone https://github.com/uwplse/StructTact.git
cd StructTact
./build.sh
cd ..

palmskog

Lemma lt_2xp1 : forall x i : nat, i < x -> 1 + 2 * i < x + x.
Proof.
Admitted.

Lemma lt_2xp : forall x i : nat, i < x -> 2 * i < x + x.
Proof.
Admitted.

Lemma lt_div2_2pow : forall n' m,  m < 2 ^ (S n') -> Nat.div2 m < 2 ^ n'.
Proof.

palmskog

(* generated by Ott 0.25 from: fitch_first_order.ott *)

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


Require Export dyadic_ordered.
Require Export FMapInterface.

palmskog

Require Import Ascii.
Require Import String.

Open Scope string_scope.

Inductive regexp :=
 | regexp_zero : regexp
 | regexp_unit : regexp
 | regexp_char (c:ascii)
 | regexp_plus (r:regexp) (r':regexp)

palmskog

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

type 'a sig0 =
  'a
  (* singleton inductive, whose constructor was exist *)



type a = char

palmskog

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

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


Import ListNotations.