Library doc

Definition Rlist : Set := List.list (cursor*element_t).

Fixpoint well_formed (l : Rlist) : Prop :=
match l with
nil => True
| a :: ls => fst a > 0 /\ has_element ls (fst a) = false /\ well_formed (ls)
end.

Fixpoint replace_element (l : Rlist) (cu : cursor) (e : element_t) : Rlist :=
match l with
   nil => nil
 | a :: ls =>
    if beq_nat (fst a) cu then (fst a, e) :: ls
    else a :: (replace_element ls cu e)
end.

Lemma WF_replace :
forall l : Rlist, forall cu : cursor, forall e : element_t,
well_formed l -> well_formed (replace_element l cu e).
  intros l cu e; induction l; simpl. (* proof by induction over l *)
  auto. (* if l is nil, the formula is trivially true *)
  case (beq_nat (fst a) cu); simpl. (* is cu equal to fst a ? *)
  intro H; exact H. (* yes -> conclusion thanks to well_formed l *)
  intros [Hfst[Hhe Hwf]]; (* no -> destruct well_formed l *)
  split; (* conclusion by splitting well_formed (replace_element l cu e) *)
  [exact Hfst|split;[|apply IHl; exact Hwf]].
  case_eq (has_element(replace_element l cu e) (fst a)); intro Hre;
  [rewrite <- Hhe; symmetry; apply (replace_has_element l cu e);
  exact Hre |reflexivity].
Qed.