Skip to content

Instantly share code, notes, and snippets.

Avatar
🐓
Hacking Coq

Anton Trunov anton-trunov

🐓
Hacking Coq
View GitHub Profile
@anton-trunov
anton-trunov / P2_omniscience.v
Last active May 24, 2017
Solution to the problem "Infinite valleys and the limited principle of omniscience"
View P2_omniscience.v
(* https://coq-math-problems.github.io/Problem2/ *)
Require Import Coq.Arith.Arith.
Require Import Coq.Classes.Morphisms.
Definition LPO := forall f : nat -> bool, (exists x, f x = true) \/ (forall x, f x = false).
Definition decr (f : nat -> nat) := forall n, f (S n) <= f n.
Definition infvalley (f : nat -> nat) (x : nat) := forall y, x <= y -> f y = f x.
View Window.idr
-- http://stackoverflow.com/questions/44079181/idris-vect-fromlist-usage-with-generated-list
total
takeExact : (n : Nat) -> (xs : List a) -> Maybe (Vect n a)
takeExact Z xs = Just []
takeExact (S n) [] = Nothing
takeExact (S n) (x :: xs) with (takeExact n xs)
takeExact (S n) (x :: xs) | Nothing = Nothing
takeExact (S n) (x :: xs) | (Just v) = Just (x :: v)
@anton-trunov
anton-trunov / P1_valley.v
Created May 18, 2017
Coq translation of a solution to the Valley Problem
View P1_valley.v
(* This is a Coq translation of this solution: https://github.com/AndrasKovacs/misc-stuff/blob/master/agda/mathprobs/p01.agda *)
(* to this https://coq-math-problems.github.io/Problem1/ *)
Require Import Coq.Arith.Arith.
Definition decr (f : nat -> nat) := forall n, f (S n) <= f n.
Definition n_valley n (f : nat -> nat) i := forall i', i' < n -> f (S (i' + i)) = f (i' + i).
Lemma is_n_valley {f} n : decr f -> forall i, n_valley n f i \/ (exists i', f i' < f i).
View RewriteUnderLambda.v
(* http://stackoverflow.com/questions/43849824/coq-rewriting-using-lambda-arguments/ *)
Require Import Coq.Lists.List. Import ListNotations.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.
Generalizable All Variables.
Instance subrel_eq_respect {A B : Type} `(sa : subrelation A RA eq)
`(sb : subrelation B eq RB) :
View SumCont.idr
--http://stackoverflow.com/questions/43879173/in-idris-use-rewrite-under-a-lambda
%default total
sum : List Nat -> Nat
sum [] = 0
sum (x :: xs) = x + sum xs
sum_cont' : {a : Type} -> List Nat -> (Nat -> a) -> a
sum_cont' [] k = k 0
View proof_using_type.v
Require Import Coq.Logic.EqdepFacts.
Set Implicit Arguments.
Inductive ext : Type :=
| ext_ : forall (X: Type), X -> ext.
Variable eqXY: forall X, X -> X -> Prop.
Inductive Eq_ext (X : Type) : ext -> ext -> Prop :=
View MutuallyInductiveTypesViaTypeFamilies.idr
%default total
data FS : (switch : Bool) -> Type where
FirstSimple : FS False
FirstSecond : FS True -> FS False
SecondSimple : FS True
SecondFirst : List (FS False) -> FS True
calculate : FS b -> Nat
calculate FirstSimple = 1
View MutInductiveExample.idr
%default total
mutual
data First = FirstSimple | FirstSecond Second
data Second = SecondSimple | SecondFirst ListFirst
data ListFirst = NilFirst | ConsFirst First ListFirst
mutual
calculateFirst : First -> Nat
calculateFirst FirstSimple = 1
View WellFoundedStep.idr
-- http://stackoverflow.com/questions/40611744/well-founded-recursion-by-repeated-division
import Data.Nat.DivMod
import Order
data Steps: (d : Nat) -> {auto dValid: d `GTE` 2} -> (n : Nat) -> Type where
Base: (rem: Nat) -> (rem `GT` 0) -> (rem `LT` d) -> (quot : Nat) -> Steps d {dValid} (rem + quot * d)
Step: Steps d {dValid} n -> Steps d {dValid} (n * d)
total
View Order.idr
module Order
%access public export
%default total
ltLte : m `LT` n -> m `LTE` n
ltLte (LTESucc x) = lteSuccRight x
ltLteTransitive : m `LT` n -> n `LTE` p -> m `LT` p
ltLteTransitive (LTESucc x) (LTESucc y) = LTESucc $ lteTransitive x y