Goal typed_ref_lemma_HeapMaximum. Hint HeapMaximum,property. Proof. Require Import Psatz. intros. (* for me it somehow easier to first proof this slight reformulation and apply it later *) assert(Reformulate: forall (i : int) (s : farray addr int) (b : addr), let x := 1 + i in 0 <= i -> P_IsHeap s b x -> P_MaxElement s b x 0). { intros n s b. intros x A. subst x. apply natlike_rec2 with (z := n); auto with zarith. { rewrite Zplus_0_r. intros. unfold P_MaxElement. split; auto with zarith. split; auto with zarith. unfold P_UpperBound_2_. unfold P_UpperBound_1_. intros. replace i0 with 0 by lia. lia. } { intros z. intros. replace (Z.succ z) with (1+z) in * by lia. assert(X: P_IsHeap s b (1+z)). { unfold P_IsHeap. intros. apply H3; auto with zarith. } assert(Y: P_MaxElement s b (1+z) 0). { apply H2; auto with zarith. } unfold P_MaxElement. unfold P_UpperBound_2_. unfold P_UpperBound_1_. split; auto with zarith. split; auto with zarith. intros. assert(less_equal: i0 < 1+z \/ i0 = 1+z) by lia. destruct less_equal as [less|equal]. { apply Y; auto with zarith. } { rewrite equal. assert(Z: s .[ shift_sint32 b (1+z)] <= s .[ shift_sint32 b (L_HeapParent (1+z))]). { apply H3; auto with zarith. } assert(ZZ: s .[ shift_sint32 b (L_HeapParent (1+z))] <= s .[ shift_sint32 b 0]). { unfold L_HeapParent. replace (1+z-1) with z by lia. apply Y; auto with zarith. apply Q_HeapBounds; lia. cut (Cdiv z 2 <= z); auto with zarith. apply Q_HeapBounds; lia. } lia. } } } replace i with (1+(i-1)) by lia. apply Reformulate; auto with zarith. replace (1+(i-1)) with i by lia. trivial. Qed.