Self-contained code for an SSReflect view issue

cancel.v

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.