wilcoxjay

Require Import PArith Omega.

Lemma unique_succ : forall a : positive, exists! b : nat, S b = Pos.to_nat a.
Proof.
  induction a.
  - destruct IHa as [b [Hb Hbunique]].
    rewrite Pos2Nat.inj_xI. 
    eexists.
    split; eauto.
    intros. omega.

wilcoxjay

Goal exists x : (nat * nat * nat), fst (fst x) = 1 /\ snd (fst x) = 2 /\ snd x = 3.
evar (x : nat).
evar (y : nat).
evar (z : nat).
eexists (?x, ?y, ?z).
simpl. eauto.
Qed.

wilcoxjay

// RUN: -typeEncoding:m -useArrayTheory
var {:layer 0,1} a:[int]int;

procedure {:yields} {:layer 1} main()
{
    var {:layer 0} {:linear "tid"} tid:int;
    var i: int;

    yield;
    while (true)

wilcoxjay

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Inductive hlist (A : Type) (B : A -> Type) : list A -> Type :=
| hnil : hlist B []
| hcons : forall a (b : B a) l (h : hlist B l), hlist B (a :: l).

Definition table (A R C : Type) (r : list R) (c : list C) : Type :=

wilcoxjay

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Inductive ilist (A : Type) (B : Type) : list A -> Type :=
| inil : ilist B []
| icons : forall a (b : B) l (h : ilist B l), ilist B (a :: l).

Definition table (A R C : Type) (r : list R) (c : list C) : Type :=

wilcoxjay

use egg::*;

type EGraph = egg::EGraph<FibLang, ConstantFold>;


define_language! {
    enum FibLang {
        "+" = Add([Id; 2]),
        "-" = Sub([Id; 2]),
        "fib" = Fib([Id; 1]),

wilcoxjay

Require Import List.
Import ListNotations.

Definition map_length {A B} (f : A -> B) :
  forall l, length (map f l) = length l.
refine (fix loop l := _).
refine (match l with
        | [] => _
        | x :: xs => _
        end).