{{ message }}

Instantly share code, notes, and snippets.

🐓
Hacking Coq

# Anton Trunov anton-trunov

🐓
Hacking Coq
Last active May 24, 2017
Solution to the problem "Infinite valleys and the limited principle of omniscience"
View P2_omniscience.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://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.
Created May 20, 2017
View Window.idr
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
 -- 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)
Created May 18, 2017
Coq translation of a solution to the Valley Problem
View P1_valley.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
 (* 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).
Created May 11, 2017
View RewriteUnderLambda.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
 (* 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) :
Last active May 10, 2017
View SumCont.idr
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
 --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
Created Feb 17, 2017
View proof_using_type.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.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 :=
Created Feb 10, 2017
View MutuallyInductiveTypesViaTypeFamilies.idr
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
 %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
Created Feb 10, 2017
View MutInductiveExample.idr
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
 %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
Created Dec 20, 2016
View WellFoundedStep.idr
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
 -- 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
Created Dec 20, 2016
View Order.idr
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
 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