Created
October 3, 2024 22:44
-
-
Save Iainmon/4d6a6e276ed25e350e110444e4ba6e8a to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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