clayrat

(** Author: Jean-François Monin, Verimag, Université Grenoble Alpes *)

(** ------------------------------------------------------------ *)
(** Similar to finite_set from itp13 with
- [odd/F1] renamed as [even/FO]
- the parameter is the cardinal
- definition of addition (to be used in even_bounded_nat)
*)

Require Import Utf8.

clayrat

(* https://github.com/thery/grobner/blob/master/grobner.v#L1222 *)
(* http://firsov.ee/noeth/ Firsov, Uustalu, Veltri, [2016] "Variations on Noetherianness" *)

From Coq Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import eqtype ssrnat seq.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

clayrat

Require Extraction.
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import ssrnat eqtype seq.

(* https://www.ps.uni-saarland.de/~smolka/drafts/icl2021.pdf#chapter.25 *)

Inductive A : Prop := AA of (True -> A).

Definition exf : A -> False.
Proof. by elim. Qed.

clayrat

From Equations Require Import Equations.
From Coq Require Import ssreflect ssrfun.
From mathcomp Require Import ssrnat.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive less_or_eq : nat -> nat -> Prop :=
| refl : forall {n k}, n = k -> less_or_eq n k
| step : forall {n k}, less_or_eq n k -> less_or_eq n k.+1.

clayrat

(** * The Bove-Capretta method

   This method involves building the graph and/or domain of a recursive
   definition and to define it by recursion + inversion on that graph,
   but not direct pattern matching. We show a difficult example
   involving nested recursive calls. *)

From Equations Require Import Equations.
From Coq Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import ssrnat eqtype.

clayrat

(** printing \2/ $\cup$ #∪# *)
(** printing <2= $\subseteq$ #&sube;# *)
(** printing forall $\forall$ #&forall;# *)
(** printing -> $\rightarrow$ #&rarr;# *)
(** printing /\ $\land$ #&and;# *)

From Coq Require Export ssreflect.
From Paco Require Import paco.
Global Set Bullet Behavior "None".

clayrat

module Cayley

-- https://doisinkidney.com/posts/2020-12-27-cayley-trees.html

import Data.Vect

foldlVec : {0 b : Nat -> Type} -> ({0 m : Nat} -> a -> b m -> b (S m)) -> b Z -> Vect n a -> b n
foldlVec f bz  []       = bz
foldlVec f bz (x :: xs) = foldlVec {b = b . S} f (f x bz) xs

clayrat

opam switch create 4.10.0.multicore \ 
  --packages=ocaml-variants.4.10.0+multicore \ 
  --repositories.multicoremlit.https://github.com/ocaml-multicore/multicore-opam.git,default 

clayrat

(* https://coq.discourse.group/t/dependent-pair-injectivity-equivalent-to-k/1112 *)
(* ported to SSReflect *)

From Coq Require Import ssreflect.

Notation Sig := existT.
Notation pi1 := projT1.
Notation pi2 := projT2.

Definition K X := forall (x : X) (e: x = x), eq_refl = e.

clayrat

module DBLev

import Data.List.Elem
import Decidable.Equality

%default total

-- from https://github.com/agda/agda/blob/master/test/Succeed/Issue985.agda

data Ty = A