wilcoxjay

Set Implicit Arguments.
Set Asymmetric Patterns.

Section Sequence.

Variable E: Set.

Inductive Sequence: nat -> Set :=
  | SequenceLeaf: E -> E -> Sequence 0
  | SequenceNode: forall n, Sequence n -> Sequence n -> Sequence (S n).

wilcoxjay

// A simple implementation of dynamically resizing arrays.

class Vector<T(==)> {
  var data: array<T>;
  var size: int;

  ghost var Repr: set<object>;
  ghost var contents: seq<T>;

  predicate Valid()

wilcoxjay

Require Import StructTact.StructTactics.
Require Import List.
Import ListNotations.

Module Monad.
  Class t (M : Type -> Type) : Type :=
    Pack
      { ret : forall {A}, A -> M A;
        bind : forall {A B}, M A -> (A -> M B) -> M B
      }.

wilcoxjay

diff --git a/src/HostedCompilerProofALU.v b/src/HostedCompilerProofALU.v
index 536866d..cade5c9 100644
--- a/src/HostedCompilerProofALU.v
+++ b/src/HostedCompilerProofALU.v
@@ -42,6 +42,66 @@ Proof.
   congruence.
 Qed.
 
+Ltac destruct_bpf_opcode x := 
+    refine 

wilcoxjay

Require Import List.
Import ListNotations.

Require Import Arith Omega.

Require Import StructTact.StructTactics.
Require Eqdep_dec.

(* heterogeneous lists. for more details see cpdt:
   http://adam.chlipala.net/cpdt/html/Cpdt.DataStruct.html *)

wilcoxjay

Lemma typing_inversion_fix3 : forall G t T,
  G |-- tfix t \in T ->
  exists U1 U2, G |-- t \in TArrow U1 U2 /\ U1 <: T /\ U2 <: T /\ U2 <: U1.

wilcoxjay

-  Case "tfix". (* JSTOLAREK : stuck here *)
-Abort.
+  Case "tfix".
+    destruct (typing_inversion_fix4 _ _ _ H) as [U1 [U2 ?]].
+    intuition.
+    eapply T_Sub with (S := U1); auto.
+    constructor.
+    eapply T_Sub with (S := TArrow U1 U2); eauto.

wilcoxjay

Fixpoint Fin (n : nat) : Type :=
  match n with
  | 0 => Empty_set
  | S n' => option (Fin n')
  end.

Definition cardinality (n : nat) (A : Type) : Prop :=
  exists (f : A -> Fin n) (g : Fin n -> A),
    (forall x, g (f x) = x) /\ (forall y, f (g y) = y).

wilcoxjay

Require Import List.
Import ListNotations.

Module member.
  Inductive t {A : Type} (x : A) : list A -> Type :=
  | Here : forall {l}, t x (x :: l)
  | There : forall {y l}, t x l -> t x (y :: l)
  .
  Arguments Here {_ _ _}.
  Arguments There {_ _ _ _} _.

wilcoxjay

Require Import List.
Import ListNotations.

Fixpoint akr_fold {A} (P : nat -> Type) (P_nil : P 0) (P_cons : forall n, A -> P n -> P (S n)) (l : list A) : P (length l) := 
  match l with
  | [] => P_nil
  | a :: l' => P_cons _ a (akr_fold P P_nil P_cons l')
  end.