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).

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.

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

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

// 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

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

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

-*- mode: compilation; default-directory: "~/build/JonPRL/" -*-
Compilation started at Thu Oct  6 17:42:16

/Users/jrw12/build/JonPRL/bin/jonprl --check bug.jonprl
In assert, goal is:
⊢ =(nat; nat; U{i})
z = h@101
term = void
term' = void
In assert, goal is:

wilcoxjay

Theorem foo : [(n : nat) -> (x : =(zero; succ(n); nat)) -> =(zero; succ(n); nat)] {
  intro; aux {auto};
  intro; aux {auto};
  hypothesis #2  ||| works just fine here
}.

Operator is-zero : (0).
[is-zero(n)] =def= [natrec(n; unit; _._. void)].

Theorem succ-not-zero : [(n : nat) -> =(succ(n); zero; nat) -> void] {

wilcoxjay

(Prog [
(Func "swap" ("a" :: "i" :: "j" :: nil)
  (Sseq 
  (Sset "tmp" (Eidx (Evar "a") (Evar "i")))
  (Sseq 
  (Swrite "a" (Evar "i") (Eidx (Evar "a") (Evar "j")))
  (Swrite "a" (Evar "j") (Evar "tmp"))))
  (Evar "a"));
(Func "reverse" ("a" :: nil)
  (Sseq