{{ message }}

Instantly share code, notes, and snippets.

🐓
Hacking Coq

Anton Trunov anton-trunov

🐓
Hacking Coq
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 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)
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 24, 2017
Full proof for my answer to https://stackoverflow.com/questions/44059569/
View nodup_app_disjoint.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://stackoverflow.com/questions/44059569/coq-goal-variable-not-transformed-by-induction-when-appearing-on-left-side-of-a/ *) Require Import Coq.Lists.List. Import ListNotations. Inductive Disjoint {X : Type}: list X -> list X -> Prop := | disjoint_nil: Disjoint [] [] | disjoint_left: forall x l1 l2, Disjoint l1 l2 -> ~(In x l2) -> Disjoint (x :: l1) l2 | disjoint_right: forall x l1 l2, Disjoint l1 l2 -> ~(In x l1) -> Disjoint l1 (x :: l2). Hint Constructors Disjoint.
Last active May 26, 2017
Solution to "Finite Cancellative Semigroups" problem
View P3_finite_cancellative_semigroups.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/Problem3/ *) Definition inj{X Y}(f : X -> Y) := forall x x', f x = f x' -> x = x'. Definition surj{X Y}(f : X -> Y) := forall y, {x : X | f x = y}. Definition ded_fin(X : Set) := forall f : X -> X, inj f -> surj f. Section df_inh_cancel_sgroups.
Last active Jun 4, 2017
A solution to https://coq-math-problems.github.io/Problem4/
View P4_injections_surjections_on_finite_sets.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/Problem4/ *) Definition inj {X Y} (f : X -> Y) := forall x x', f x = f x' -> x = x'. Definition surj {X Y} (f : X -> Y) := forall y, {x : X | f x = y}. Definition left_inv {X Y} (g : Y -> X) (f : X -> Y) := forall x, g (f x) = x. Definition right_inv {X Y} (g : Y -> X) (f : X -> Y) := left_inv f g.
Created Jun 18, 2017
View make_diff.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://stackoverflow.com/questions/44612214/how-to-deal-with-really-large-terms-generated-by-program-fixpoint-in-coq *) Require Import Coq.Lists.List. Import ListNotations. Require Import Coq.Relations.Relations. Require Import Coq.Program.Program. Definition is_decidable (A : Type) (R : relation A) := forall x y, {R x y} + {~(R x y)}. Definition eq_decidable (A : Type) := forall (x y : A), { x = y } + { ~ (x = y) }.
Created Sep 19, 2017
View forw_rev_list_ind.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.Arith.Arith. Require Import Coq.Lists.List. Import ListNotations. Lemma forw_rev_list_ind {A} (P : list A -> Prop) (Pnil : P []) (Psingle : (forall a, P [a])) (Pmore : (forall a b, forall xs, P xs -> P ([a] ++ xs ++ [b]))) (xs : list A)
Created Mar 20, 2018
Self-contained code for an SSReflect view issue
View cancel.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
 From Coq Require Import ssreflect ssrfun ssrbool List. Import ListNotations. Set Implicit Arguments. Unset Strict Implicit. Section Heap. Definition heap := nat. Definition valid (h : heap) : bool := true. Definition empty : heap := 0. Definition join (h1 h2 : heap) := nosimpl (h1 + h2).
Created Mar 28, 2018
View tuple_rev_involutive.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
 From Coq Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import eqtype seq tuple. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Definition trev T n (t : n.-tuple T) := [tuple of rev t]. Lemma trevK T n : involutive (@trev T n). Proof. by move=>t; apply: val_inj; rewrite /= revK. Qed.