anton-trunov

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.

anton-trunov

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

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

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

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

%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

%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

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

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

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