Commit 7455d45f authored by Dan Frumin's avatar Dan Frumin

Prove base case for memcpy

parent 283947ec
......@@ -41,18 +41,25 @@ Section memcpy.
vcg_solver. iNext. iIntros (?) "[% Hpp]"; simplify_eq/=.
iExists (p.1,p.2+i)%nat,(p.1,p.2+length ls1)%nat; repeat iSplit; eauto.
destruct (decide (i < length ls1)).
destruct (decide (i < length ls1)%nat).
- iLeft. iSplit.
{ iPureIntro. compute[cloc_lt]. f_equal. simpl.
rewrite !bool_decide_true; auto. omega. }
eapply tac_vcg_sound.
apply _. (* Separate the - ↦ - propositions out of the context*)
compute; reflexivity. (* Compute the known locations *)
apply _. (* Compute the symbolic environment based on known locations *)
apply _. (* Reify the expression *)
done. (* Prove that the environment is well-formed *)
rewrite bool_decide_true; auto. split; auto. omega. }
- iRight. iSplit.
{ iPureIntro. compute[cloc_lt]. f_equal. simpl.
rewrite bool_decide_false; auto. intros [? ?]. omega. }
iApply a_seq_spec. iModIntro.
assert (ls1 = ls2) as ->.
{ generalize dependent i. generalize dependent ls2. induction ls1; simpl; eauto.
- intros ls2 ->%nil_length_inv. done.
- simpl. intros ls2 Hlen i Htake Hi.
induction ls2; simpl; eauto. inversion Hlen.
apply Nat.nlt_succ_r in Hi. destruct i as [|i]; first inversion Hi.
simpl in Htake. simplify_eq/=. f_equal. eapply IHls1; eauto.
intros ?%Nat.nlt_succ_r. done. }
Lemma memcpy_spec (p q : cloc) (n : nat) (ls1 ls2 : list val) R :
length ls1 = n
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment