Skip to content

Instantly share code, notes, and snippets.

Avatar
🐓
Hacking Coq

Anton Trunov anton-trunov

🐓
Hacking Coq
View GitHub Profile
View fib_manual.v
Require Import Arith.
Fixpoint fib_v1 (n : nat) : nat :=
match n with
| 0 => O
| S n' => match n' with
| O => 1
| S n'' => (fib_v1 n') + (fib_v1 n'')
end
end.
View log2n.v
Definition log2 n :=
let helper :=
(fix log2_helper n dummy :=
match dummy with
| 0 => 0
| S d' => match n with
| 0 | 1 => 0
| n => S (log2_helper (Nat.div2 n) d')
end
end) in
View log2_well_founded_induction.v
Definition log2 :=
well_founded_induction Wf_nat.lt_wf (fun _ => nat)
(fun n => match n return ((forall y : nat, (y < n) -> nat) -> nat) with
| 0 => fun _ => 0
| 1 => fun _ => 0
| n => fun self => S (self (Nat.div2 n)
(Nat.lt_div2 _ (lt_0_Sn _)))
end).
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
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 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 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 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 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 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) :