Skip to content

Instantly share code, notes, and snippets.

Avatar
💭
keep_learning

Mukesh Tiwari mukeshtiwari

💭
keep_learning
View GitHub Profile
@mukeshtiwari
mukeshtiwari / AwesomeListLemmas.v
Created April 27, 2023 12:25 — forked from Agnishom/AwesomeListLemmas.v
Awesome List Lemmas
View AwesomeListLemmas.v
(*
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.
View Tmp.v
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,
View Tmp.v
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.
View Vector_rev.v
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.
View Tmp.v
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).
View Coqmailing.v
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.
View Tw.v
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.
View Knaster_Tarski.v
(*
Dominique code from the Coq mailing list
*)
Section KNASTER_TARSKI.
Variable A: Type.
View Thomas.v
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.
View Monin.v
https://www-verimag.imag.fr/~monin/Proof/