mukeshtiwari

(* 
  
  Some lemmas that can be used in conjunction with those in Coq.Lists.List
  
  See https://coq.inria.fr/library/Coq.Lists.List.html
 
 *)

Require Import Lia.
Require Import Coq.Lists.List.

mukeshtiwari

Notation "a =S= b"   := (brel_set  (brel_product eqA eqP) a b = true) (at level 70).
  

  (* = or =S=, both are fine! *)
  Lemma iterate_minset_inv_2 : 
    forall (X W Y : finite_set (A * P)) au bu,
    find (theory.below (manger_pre_order lteA) (au, bu)) X = None -> 
    find (theory.below (manger_pre_order lteA) (au, bu)) Y = None ->
    (* 
    (∀ t : A * P,

mukeshtiwari

Require Import Lia
  Coq.Unicode.Utf8
  Coq.Bool.Bool 
  Coq.Init.Byte
  Coq.NArith.NArith
  Coq.Strings.Byte
  Coq.ZArith.ZArith
  Coq.Lists.List.
  
Import Notations ListNotations.

mukeshtiwari

Require Import Coq.Vectors.Vector.
Import VectorNotations.

Fixpoint vappend {T : Type} {n m} (v1 : t T n) (v2 : t T m)
  : t T (plus n m) :=
  match v1 in t _ n return t T (plus n m) with
  | [] => v2
  | x :: v1' => x :: vappend v1' v2
  end.

mukeshtiwari

Definition bind_vector :
    forall {m n : nat}, Vector.t (A * prob) (1 + m) ->
    list (Vector.t A n * prob)  -> list (Vector.t A (S n) * prob).
  Proof.
    refine(
      fix bind_vector m :=
      match m with 
      | 0 => fun n ca cb => _
      | S m' => fun n ca cb => _ 
      end).

mukeshtiwari

From Coq Require Import Arith Utf8 Psatz
  Peano.
  
Section Wf_div.

 
  Theorem nat_div :  nat -> forall (b : nat),
    0 < b -> nat * nat.
  Proof.
    intro a.

mukeshtiwari

Section Wf.

  Variables 
    (A : Type)
    (R : A -> A -> Prop).

  Inductive Acc (x: A) : Prop :=
    Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.

mukeshtiwari

(* 
  
  Dominique code from the Coq mailing list 
  
 *)

Section KNASTER_TARSKI.

Variable A: Type.

mukeshtiwari

From mathcomp Require Import 
all_ssreflect algebra.matrix
algebra.ssralg.
Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import 
eqtype fingroup fintype ssrnat seq finalg ssralg.   
From mathcomp Require Import 
bigop gproduct finset div.

mukeshtiwari

https://www-verimag.imag.fr/~monin/Proof/