Skip to content

Instantly share code, notes, and snippets.

@anton-trunov

anton-trunov/log2_well_founded_induction.v

Created November 23, 2016 12:03
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save anton-trunov/c9e6bd31d26b24e63349a9e217a1f9f4 to your computer and use it in GitHub Desktop.
Save anton-trunov/c9e6bd31d26b24e63349a9e217a1f9f4 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment