anton-trunov

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

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

anton-trunov

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

anton-trunov

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

anton-trunov

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 :=

anton-trunov

%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

anton-trunov

%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

anton-trunov

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

anton-trunov

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

anton-trunov

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).