codyroux

module Map = Map.Make(String)

type ref_pointer = int
(* The type of values, that is the output of a terminating computation *)
type value = Int of int | Clos of env * term | Ref of ref_pointer
(* The type of programs *)
and term = Var of string
         | Let of string * term * term
         | Print of term
         | Lit of int

codyroux

mutual
inductive Subst : Type where
| ids : Subst
| tcons : Term → Subst → Subst
| shift : Subst
| comp : Subst → Subst → Subst
inductive Term : Type where
| var : Term
| lam : Term → Term

codyroux

#include <stdio.h>
#include <stdlib.h>

#define MEM_SIZE 1000000000 //10^9

struct mem_array {
  size_t buff_size;
  char * addr;
};

codyroux

type term =
  | Var of int
  | Num of int
  | App of term * term
  | Lam of term
  | Plus of term * term
  | Ite of term * term * term

type input = { mutable pos : int; mutable str : string }

codyroux

Require Import Lia.

Section Iter_to_ind.

  Variable B : Prop.
  Variable F : Prop -> Prop.

  Hypothesis F_ext : forall P Q, (P <-> Q) -> (F P <-> F Q).
  
  Fixpoint iter_prop (n : nat) : Prop :=

codyroux

Notation "P ≢ Q" := (~(P <-> Q))(at level 100).

Theorem no_middle : ~(exists P, (P ≢ True) /\ (P ≢ False)).
Proof.
  intro h.
  destruct h as [P [h1 h2]].
  apply h2.
  split; [ | intros h; contradiction].
  intros h3.
  apply h1; split; auto.

codyroux

Require Import Setoid.


Axiom is_a_neg : forall (P : Prop), exists (Q : Prop), P <-> ~Q.

Lemma not_not : forall P, ~~P -> P.
Proof.
  intros P.
  assert (h := is_a_neg P); destruct h as [Q h].
  rewrite h.

codyroux

(* A relatively straightforward formalization of HA^2 *)

Require Import Coq.Lists.List.
Require Import Coq.Strings.String.

Inductive tm :=
| v(name : string)
| Succ(a : tm)
| Z
| Plus(a b : tm)

codyroux

(*

Ideas:
I'm borrowing generously from https://xavierleroy.org/talks/compilation-agay.pdf and
https://github.com/ajcave/code/blob/master/normalization/weak-head-bigstep-cbn.agda

But CBV.


*)

codyroux

(*

Ideas:
1. Strong reduction (ugh): Keep computing through lambdas. Most straightforward, but annoying, need to reason about db even more
2. Computability take an eval context as well, so that all predicates are "up to substitution".
   Problem: how to we deal with "computable contexts"?
   E.g. aplications: Do they thake the previous elements in the env or not?
   Does "positive" style predicates help?
3. Screw this and go with names.
4. Reason about only closed terms (somehow?) Not sure how to formulate the main lemma.