clayrat

module Const

import Interfaces.Verified

%default total

data Const : Type -> Type -> Type where
  MkConst : a -> Const a b

getConst : Const a b -> a

clayrat

Section ProdSum.

Variables A B C : Prop.

Class Isomorphism A B :=
  MkIsomorphism {
    from: A -> B;
    to: B -> A;
    from_to b: from (to b) = b;
    to_from a: to (from a) = a

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

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

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

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

(** 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

(** * 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

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

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.