mbrcknl

(*
  Circular doubly-linked lists.
  Each list is accessed via a cursor that owns the whole structure.
  Operations: insert, delete, fold, cursor movement forward and backward.
*)

From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Export proofmode.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation array.

mbrcknl

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
 
{-# OPTIONS_GHC -Wall #-}
 
data HList f l where
  HNil :: HList f '[]

mbrcknl

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilyDependencies #-}

data Ty = IntTy | FunTy Ty Ty

mbrcknl

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}

data Ty = IntTy | FunTy Ty Ty

data Term :: (Ty -> *) -> Ty -> * where
  Lit :: Int -> Term var IntTy

mbrcknl

theory locale_experiment
imports Main
begin

section \<open>Algebraic formulation of a semilattice\<close>

locale semigroup =
  fixes ap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes assoc: "\<And>x y z. ap x (ap y z) = ap (ap x y) z"

mbrcknl

theory Scratch imports Main begin

locale Magma =
  fixes m :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"

locale SemiGroup = Magma +
  assumes assoc: "\<And>x y z. m (m x y) z = m x (m y z)"

locale Commutative = Magma +
  assumes comm: "\<And>x y. m x y = m y x"

mbrcknl

Definition p5 : com :=
  WHILE (BNot (BEq (AId X) (ANum 1))) DO
    HAVOC X
  END.

Definition p6 : com :=
  X ::= ANum 1.

Lemma p5_may_terminate: forall s, p5 / s || update s X 1.
  intro s; destruct (eq_nat_dec (s X) 1).

mbrcknl

Require Import List.

Inductive type : Type :=
| base : type
| arr  : type -> type -> type.

Infix "==>" := arr (right associativity, at level 52).

Inductive elem {A: Type} (x: A): list A -> Type :=
| here  : forall xs, elem x (x :: xs)

mbrcknl

Require Import Sorted.
Require Import Permutation.

Definition isSortingFunction (A: Type) (R: A -> A -> Prop) (f: list A -> list A): Prop :=
  forall (xs: list A), Permutation xs (f xs) /\ Sorted R (f xs).

Check (isSortingFunction: forall (A: Type), (A -> A -> Prop) -> (list A -> list A) -> Prop).

mbrcknl

Require Import List.

Inductive type : Type :=
| base : type
| arr  : type -> type -> type.

Infix "==>" := arr (right associativity, at level 52).

Inductive elem {A: Type} (x: A): list A -> Type :=
| here  : forall xs, elem x (x :: xs)