Докажите свойство кучи (подмножество и равенство) в логике разделения, используя Coq - PullRequest
Новая
       18

Докажите свойство кучи (подмножество и равенство) в логике разделения, используя Coq

0 голосов
/ 22 декабря 2018

Я хочу доказать две леммы в coq, чтобы они были полезны для дальнейших доказательств.Я уже думал об этом в течение нескольких часов (> = 4 часа).Я хочу получить некоторые подсказки или частичные или полные доказательства лемм ниже.(Эти леммы о логике разделения.) 

Lemma imply_subset: forall (h1 h2 h: heap), 
  h_union h1 h2 = h -> disjoint h1 h2 -> h_subset h2 h.
Proof.
  Admitted.

Lemma heap_equality1: forall (h1 h2 h h11: heap),
  disjoint h1 h2 -> disjoint h11 h2 -> 
    h_union h1 h2 = h -> h_union h11 h2 = h -> h1 = h11.
Proof.
  Admitted.

Ниже приведены некоторые определения. 

(* if heap maps a natural number (address) to
None, we say the address is not a valid address,
or it is not in the domain of the heap *)

Definition heap := nat -> option nat.

(* h1 and h2 have disjoint domain *)
Definition disjoint (h1 h2: heap) : Prop := 
  forall l, not_in_dom l h1 \/ not_in_dom l h2.

(* union of two heaps *)
Definition h_union (h1 h2: heap) : heap :=
  fun l => 
    if (in_not_in_dec l h1) then h1 l else h2 l.

(* h1 is a subset of h2 *)
Definition h_subset (h1 h2: heap) : Prop := 
  forall l n, h1 l = Some n -> h2 l = Some n.
...