Skip to content

Instantly share code, notes, and snippets.

@Iainmon
Created October 3, 2024 22:44
Show Gist options
  • Save Iainmon/4d6a6e276ed25e350e110444e4ba6e8a to your computer and use it in GitHub Desktop.
Save Iainmon/4d6a6e276ed25e350e110444e4ba6e8a to your computer and use it in GitHub Desktop.
Ltac save h1 h2 :=
(*pose proof h1 as h2*)
let t := type of h1 in
assert (h2 : t) by (exact h1).
Tactic Notation "save" constr(h1) "as" ident(h2) :=
save h1 h2.
(* Ltac replace_equivalent a b p :=
let at := type of a in
let bt := type of b in
match type of p with
| at <-> bt => *)
Require Import List.
Import ListNotations.
Fixpoint map {X Y:Type} (f:X -> Y) (l:list X) : (list Y) :=
match l with
| [] => []
| x :: l' => (f x) :: (map f l')
end.
Fixpoint drop {A : Type} (n : nat) (l : list A) : list A :=
match n with
| 0 => l
| S n' => drop n' (tail l)
end.
Fixpoint In {A : Type} (x : A) (l : list A) : Prop :=
match l with
| [] => False
| x' :: l' => x = x' \/ In x l'
end.
Inductive elementhood {A : Type} : A -> list A -> Prop :=
| element_of : forall a l, In a l -> elementhood a l.
Notation "a '∈' l" := (elementhood a l) (at level 70).
Theorem in_equiv:
forall (A : Type) (x : A) (l : list A),
In x l <-> x ∈ l.
Proof.
intros A x l.
split.
- apply element_of.
- intros H1. destruct H1. assumption.
Qed.
Lemma test:
forall (A : Type) (a : A) (l : list A),
In a l -> In a (a :: l).
Proof.
intros A a.
intros l.
intros H.
destruct l.
- simpl. left. reflexivity.
- simpl. left. reflexivity.
Qed.
Lemma if_In_then_drop_head:
forall (A : Type) (l : list A) (x : A),
In x l ->
exists n l', drop n l = x :: l'.
Proof.
intros A l x.
intros H1.
induction l.
- simpl in H1. contradiction.
- simpl in H1.
destruct H1 as [ H1_1 | H1_2 ].
+ rewrite <- H1_1.
exists 0,l.
reflexivity.
+ apply IHl in H1_2 as H2.
save H2 as H3.
destruct H3 as [m [l1 H4]].
exists (S m).
exists l1.
simpl.
assumption.
Qed.
Lemma In_map:
forall (A B : Type) (f : A -> B) l x,
In x l -> In (f x) (map f l).
Proof.
intros A B f l x.
intros H1.
generalize dependent l.
induction l.
(* all: try (unfold In; left; auto). *)
- unfold In. simpl. contradiction.
- intros H2. simpl.
save H2 as H3. simpl in H3.
destruct H3 as [ H4 | H5 ].
+ left. rewrite H4. reflexivity.
+ right. apply IHl in H5. assumption.
Qed.
Lemma in_app_iff:
forall (A : Type) (x : A) l1 l2,
In x (l1 ++ l2) <-> In x l1 \/ In x l2.
Proof.
intros A x l1 l2.
split; intros H1.
- induction l1.
+ simpl in H1. right. assumption.
+ simpl in H1.
destruct H1 as [H2 | H3].
* left. rewrite H2. simpl. left. reflexivity.
* save IHl1 as H4.
apply H4 in H3 as H5.
destruct H5 as [H6 | H7].
-- left. simpl. right. assumption.
-- right. assumption.
- induction l1; destruct H1 as [H2 | H3]; simpl.
+ simpl. contradiction.
+ assumption.
+ destruct H2.
-- left. assumption.
-- assert (H3 : In x l1 \/ In x l2).
{ left. assumption. }
apply IHl1 in H3. right. assumption.
+ right.
assert (H4: In x l1 \/ In x l2).
{ right. assumption. }
apply IHl1. right. assumption.
Qed.
Definition subseq {A : Type} (l1 l2 : list A) : Prop :=
forall x, In x l1 -> In x l2.
Notation "l1 '⊆' l2" := (subseq l1 l2) (at level 70).
Lemma subseq_refl:
forall (A : Type) (l : list A),
l ⊆ l.
Proof.
intros A l.
unfold subseq.
intros x.
intros H1.
assumption.
Qed.
Lemma in_split:
forall (A : Type) (x : A) l,
In x l ->
exists l1 l2,
l = l1 ++ x :: l2.
Proof.
intros A x l.
intros H1.
induction l as [| x' l' IHl'].
- unfold In in H1.
contradiction.
- unfold In in H1.
destruct H1 as [H1_1 | H1_2].
+ exists [].
exists l'.
simpl.
rewrite H1_1.
reflexivity.
+ assert (H4 : In x l').
{ apply H1_2. }
pose proof (IHl' H4) as H5.
pose proof H5 as H6.
destruct H5 as [l3 [l4 H5]].
exists (x' :: l3).
exists l4.
simpl.
rewrite H5.
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment