View AwesomeListLemmas.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* | |
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* | |
Dominique code from the Coq mailing list | |
*) | |
Section KNASTER_TARSKI. | |
Variable A: Type. |
View Thomas.v
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
https://www-verimag.imag.fr/~monin/Proof/ |
NewerOlder