wilcoxjay

Section alkabetz.
  Ltac eq_apply H :=
    match type of H with 
    | ?F ?X => 
      match goal with 
      | [  |- ?F ?Y ] => 
        replace Y with X; [exact H|]
      end
    end.
  

wilcoxjay

Require Export FMapAVL.
Require Export Coq.Structures.OrderedTypeEx.

Module M := FMapAVL.Make(Nat_as_OT).

Definition ForallHashTable_ {A} (Q : A -> Prop) (h : M.t A) :=
  forall k v, M.MapsTo k v h -> Q v.

Lemma ForallHashTableEmpty_ : forall {A} (Q : A -> Prop),
                                ForallHashTable_ Q (M.empty _).

wilcoxjay

Require Import Arith.
Section vanila.

Variable A B : Type.
Variable lift : nat -> B -> A.
Variable u v n : nat.
Variable var : nat -> B.
Variable a : A.

Goal lift (S u) (if le_gt_dec v n then var (S n) else var n) = a.

wilcoxjay

Theorem necessity : 
  forall T (f : T -> nat -> T), 
    (forall b t, fold b f t = fold' b f t) -> 
    (forall b n1 n2, f (f b n1) n2 = f (f b n2) n1).

wilcoxjay

(* this file should be pasted at the bottom of core/Util.v *)

Require Import OrderedType.

Fixpoint fin_to_nat {n : nat} : fin n -> nat :=
  match n with
  | 0 => fun x : fin 0 => match x with end
  | S n' => fun x : fin (S n') => 
             match x with 
             | None => 0

wilcoxjay

Section structural_example.
  Variable A B : Type.
  Variable f g : A -> B.
  Variable Q : B -> Prop.

  Definition eg : Prop := 
    (forall x, Q (g x)) -> 
    (forall x, f x = g x) -> 
    forall x, Q (f x). 

wilcoxjay

Require Import List.
Import ListNotations.

Section redlizard.
  Variable A : Type.
  Variable P : A -> Prop.
  Hypothesis P_dec : forall x : A, {P x} + {~ P x}.
  

  Fixpoint getP' (l : list A) : (exists x, In x l /\ P x) -> {x : A | P x}.

wilcoxjay

Require Import List.
Import ListNotations.

Section rrika.
  Variable A : Type.
  Variable P : A -> Prop.
  Hypothesis P_dec : forall x : A, {P x} + {~ P x}.
  

  Fixpoint getP' (l : list A) : (exists x, In x l /\ P x) -> {x : A | P x} :=

wilcoxjay

Require Import Sorted.
Require Import List.
Import ListNotations.

Section sorted_pi. 
  Variable A : Type.
  Variable R : A -> A -> Prop.

  Hypothesis R_pi : forall a1 a2 (pf pf' : R a1 a2), pf = pf'.

wilcoxjay

Fixpoint subst_exp {b} (e : exp_ b) {struct e} : list (var * exp_ b) -> exp_ b :=
    match e with
    | e_var v => fun E =>
        match Metatheory.get v E with
        | Some e' => e'
        | None => e_var v
        end
    | e_field e0 f => fun E => e_field (subst_exp e0 E) f
    | e_meth e0 m es => fun E => e_meth (subst_exp e0 E) m (List.map (fun e => subst_exp e E) es)
    | e_new C es => fun E => e_new C (List.map (fun e => subst_exp e E) es)