roconnor

(* This Normalization by Evaluation is based on mietek's <https://research.mietek.io/A201801.FullIPLNormalisation.html>.
   I've removed the continuations to give a purely tree-based implementation.
   This is operationally less efficent than using continuations, but it is hopefully easier to understand and potentially easier to verify correct.

   Checked with Coq 8.18.0
*)

Inductive Form :=
| Zero : Form
| One : Form

roconnor

Require Import Arith.
Require Import Omega.

Set Primitive Projections.
Set Implicit Arguments.

Inductive binTree : Set :=
| Leaf : binTree
| Branch : binTree -> binTree -> binTree.

roconnor

(* In relation to https://cstheory.stackexchange.com/questions/40631/how-can-you-build-a-coinductive-memoization-table-for-recursive-functions-over-b *)
Require Import Vectors.Vector.
Import VectorNotations.

Set Primitive Projections.
Set Implicit Arguments.

Inductive binTree : Set :=
| Leaf : binTree
| Branch : binTree -> binTree -> binTree.

roconnor

// Define Computably Enumerable (aka recursively enumerable) predicates.
CESet : (Nat -> o) -> o
CESet := \p. exists f \in PRF2Set. p = (\n. exists m:Nat. 0 < f n m)

// Standard Model
  
interpT : (Nat -> Nat) -> Term -> Nat
interpT := \v. TermR_(Nat) v 0 (\t. S) (\t. \s. \n, \m. n + m) (\t. \s. \n. \m. n * m)

interpF : (Nat -> Nat) -> Formula -> o

roconnor

Require Import Bvector.
Require Import Eqdep_dec.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Definition bCompare (x y : bool) : comparison :=
match x, y with
| false, false => Eq