leodemoura

universe u

variable {A : Type u}
/- Anonymous instance variables are automatically added
   when their parameters are used in a declaration -/
variable [has_add A]
variable [has_sub A]
variable [s : has_mul A]

def f (a : A) : A :=

leodemoura

universes u

def bitvector (sz : nat) : Type :=
{ n : nat // n < 2^sz }

/- We use `by apply bv_mod_lt` to discharge the property above in
   many bitvector definitions. -/
lemma bv_mod_lt (n : nat) (sz : nat) : n % (2^sz) < 2^sz :=
begin
  apply nat.mod_lt,

leodemoura

import data.rbmap

namespace experiment

def prog (σ : Type) (α : Type) :=
state_t σ option α

instance (σ : Type) : monad (prog σ) :=
by delta prog; apply_instance

leodemoura

import data.rbmap

namespace experiment

def prog (σ : Type) (α : Type) :=
state_t σ option α

instance (σ : Type) : monad (prog σ) :=
by delta prog; apply_instance

leodemoura

import data.rbmap

universes u v
variables {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt]

def map_equiv (m₁ m₂ : rbmap α β lt) : Prop :=
∀ a : α, m₁.find a = m₂.find a

local infix ` ≈ `:50 := map_equiv

leodemoura

namespace experiment

def prog (σ : Type) (α : Type) :=
state_t σ option α

instance (σ : Type) : monad (prog σ) :=
by delta prog; apply_instance

variables {σ α β : Type}

leodemoura

namespace design_1

structure wp_state (σ : Type) (α : Type) :=
/- wp is a function that converts a postcondition into a predcondition. -/
(wp     : (α × σ → Prop) → σ → Prop)
(action : σ → α × σ)
(valid  : ∀ (post : α × σ → Prop) (s : σ), (wp post) s → post (action s))


namespace wp_state

leodemoura

inductive term
| const (c : string)                   : term
| app   (fn : string) (ts : list term) : term

mutual inductive is_rename, is_rename_lst
with is_rename : term → string → string → term → Prop
| const_eq (c₁ c₂) : is_rename (term.const c₁) c₁ c₂ (term.const c₂)
| const_ne (c₁ c₂ c₃) (hne : c₁ ≠ c₂) : is_rename (term.const c₁) c₂ c₃ (term.const c₁)
| app      (fn c₁ c₂ ts₁ ts₂) (h₁ : is_rename_lst ts₁ c₁ c₂ ts₂) : is_rename (term.app fn ts₁) c₁ c₂ (term.app fn ts₂)

leodemoura

universes u v

inductive rbnode.color
| red
| black

open rbnode.color nat

inductive rbnode (α : Type u) : color → nat → Type u
| leaf {}                                                                      : rbnode black 0

leodemoura

universes u v
variables {α : Type u} {β : Type v}

@[congr] lemma map_congr (f₁ f₂ : α → β) : ∀ (l₁ l₂ : list α), l₁ = l₂ → (∀ a, a ∈ l₁ → f₁ a = f₂ a) → l₁.map f₁ = l₂.map f₂ :=
begin
  intros l₁ l₂ h,
  subst h,
  induction l₁ with a₁ l₁,
  {intros, refl},
  {intro h,