Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Self-contained code for an SSReflect view issue
From Coq Require Import ssreflect ssrfun ssrbool List.
Import ListNotations.
Set Implicit Arguments.
Unset Strict Implicit.
Section Heap.
Definition heap := nat.
Definition valid (h : heap) : bool := true.
Definition empty : heap := 0.
Definition join (h1 h2 : heap) := nosimpl (h1 + h2).
End Heap.
Notation "h1 :+ h2" := (join h1 h2) (at level 43, left associativity).
Section ReflectExpr.
Definition ctx := list heap.
Definition empc : ctx := [].
Definition synheap := list nat.
Definition einterp := [fun (c : ctx) n => nth n c empty].
Fixpoint interp (c : ctx) (t : synheap) : heap :=
match t with
| [] => empty
| [v] => einterp c v
| e :: t' => einterp c e :+ interp c t'
end.
Definition fact : Type := synheap * synheap.
Definition eval_fact (c : ctx) (f : fact) : Prop :=
let (h1,h2) := f in interp c h1 = interp c h2.
Fixpoint eval (c : ctx) (s : list fact) : Prop :=
match s with
| [] => True
| [f] => eval_fact c f
| f :: fs => eval_fact c f /\ eval c fs
end.
Fixpoint cancel' (c : ctx) (t1 t2 r : synheap) : list fact :=
match t1 with
| [] => match r, t2 with
| [], [] => []
| _ , _ => [(r, t2)]
end
| h :: t1' =>
if existsb (fun x => Nat.eqb h x) t2
then cancel' c t1' (filter (predC (Nat.eqb h)) t2) r
else cancel' c t1' t2 (h :: r)
end.
Definition cancel c t1 t2 := cancel' c t1 t2 [].
End ReflectExpr.
Section XFind.
Variable A : Type.
Structure xtagged := XTag {xuntag :> A}.
Definition extend_tag := XTag.
Definition recurse_tag := extend_tag.
Canonical Structure found_tag x := recurse_tag x.
Structure xfind (s r : list A) (i : nat) := XFind { elem_of :> xtagged }.
Arguments XFind : clear implicits.
Canonical Structure found_struct x t :=
XFind (x :: t) (x :: t) 0 (found_tag x).
Canonical Structure recurse_struct i y t r (f : xfind t r i) :=
XFind (y :: t) (y :: r) (S i) (recurse_tag f).
Canonical Structure extend_struct x :=
XFind [] [x] 0 (extend_tag x).
End XFind.
Section HeapReflection.
Structure tagged_heap := Tag {untag :> heap}.
Definition var_tag := Tag.
Canonical Structure union_tag hc := var_tag hc.
Structure ast (i j : ctx) (t : synheap) := Ast {heap_of :> tagged_heap}.
Arguments Ast : clear implicits.
Canonical Structure union_struct i j k t1 t2 (f1 : ast i j t1) (f2 : ast j k t2) :=
Ast i k (t1 ++ t2) (union_tag (f1 :+ f2)).
Canonical Structure var_struct hs1 hs2 n (xf : xfind hs1 hs2 n) :=
Ast hs1 hs2 [n] (var_tag (xuntag xf)).
End HeapReflection.
Theorem cancelR j k t1 t2 (f1 : ast empc j t1) (f2 : ast j k t2) :
valid f1 ->
untag (heap_of f1) = untag (heap_of f2) ->
eval k (cancel k t1 t2).
Admitted.
Example stress
(h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 : heap) :
valid (h1 :+ h2 :+ h3 :+ h4 :+ h5 :+ h6 :+ h7 :+ h8 :+ h9 :+ h10 :+ h11 :+ h12 :+ h13 :+ h14 :+ h15) ->
h1 :+ h2 :+ h3 :+ h4 :+ h5 :+ h6 :+ h7 :+ h8 :+ h9 :+ h10 :+ h11 :+ h12 :+ h13 :+ h14 :+ h15
=
h1 :+ h2 :+ h3 :+ h4 :+ h5 :+ h6 :+ h7 :+ h8 :+ h9 :+ h10 :+ h11 :+ h12 :+ h13 :+ h16 ->
h15 :+ h14 = h16.
move=>D.
Time move/(cancelR D)=>/=->. (* 4 secs on my machine *)
Restart.
move=>D H.
Time move: (cancelR D H)=>/=->. (* 0.3 secs on my machine *)
by [].
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment