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.
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.