Complete this form and hit the "Save Changes" button!
No ratings
Are you sure you want to delete this code? Please type DELETE in the box below to confirm.
Are you sure you want to verify this code?
Are you sure you want to publish this code?
Are you sure you want to unpublish this code?
Are you sure you want to autogenerate the summary + description for this code?
xxxxxxxxxx
Require Import List.
Import ListNotations.
Require Import StructTact.StructTactics.
Require Import StructTact.ListTactics.
Fixpoint before_all {A : Type} (x : A) y l : Prop :=
match l with
| [] => True
| a :: l' =>
~ In x l' \/
(y <> a /\ before_all x y l')
end.
Section before_all.
Variable A : Type.
Lemma before_all_head_not_in :
forall l (x y : A),
x <> y ->
before_all x y (y :: l) ->
~ In x l.
Proof using.
intros.
simpl in *.
break_or_hyp; auto.
break_and. auto.
Qed.
Lemma before_all_neq_append :
forall l (x y a : A),
a <> x ->
before_all x y l ->
before_all x y (l ++ [a]).
induction l.
- intros; left; auto.
- intros;
break_or_hyp.
* left.
intro H_in.
do_in_app.
* break_and.
right.
split; auto.
Lemma before_all_not_in_1 :
~ In x l ->
before_all x y l.
destruct l; simpl in *; auto.
Lemma before_all_not_in_2 :
~ In y l ->
- intros. simpl in *. auto.
- intros. simpl in *.
assert (H_neq: y <> a); auto.
assert (H_in: ~ In y l); auto.
End before_all.
