baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-12-05 09:00:44 +01:00
parent 9fe0252398
commit 7051b17c49
1 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
src/mapping.v
View File

@ -46,14 +46,14 @@ Qed.
*) *)
Lemma permutation_mapping_nil {X: Type} : Lemma Permutation_mapping_nil {X: Type} :
forall (base : list X), Permutation_mapping nil nil base. forall (base : list X), Permutation_mapping nil nil base.
Proof. Proof.
intro base. exists base. exists nil. split; easy. intro base. exists base. exists nil. split; easy.
Qed. Qed.
Lemma permutation_mapping_nil_l {X: Type} : Lemma Permutation_mapping_nil_l {X: Type} :
forall (u base : list X), Permutation_mapping nil u base -> u = nil. forall (u base : list X), Permutation_mapping nil u base -> u = nil.
Proof. Proof.
intro u. induction u; intro base; intro H. reflexivity. intro u. induction u; intro base; intro H. reflexivity.
@ -63,7 +63,7 @@ Proof.
Qed. Qed.
Lemma permutation_mapping_nil_r {X: Type} : Lemma Permutation_mapping_nil_r {X: Type} :
forall (u base : list X), Permutation_mapping u nil base -> u = nil. forall (u base : list X), Permutation_mapping u nil base -> u = nil.
Proof. Proof.
intro u. induction u; intro base; intro H. reflexivity. intro u. induction u; intro base; intro H. reflexivity.
@ -73,7 +73,7 @@ Proof.
Qed. Qed.
Lemma permutation_mapping_cons {X: Type} : Lemma Permutation_mapping_cons {X: Type} :
forall (u v base : list X) a b, forall (u v base : list X) a b,
Permutation_mapping (a::u) (b::v) base -> Permutation_mapping u v base. Permutation_mapping (a::u) (b::v) base -> Permutation_mapping u v base.
Proof. Proof.
@ -83,7 +83,7 @@ Proof.
Qed. Qed.
Lemma permutation_mapping_app {X: Type} : Lemma Permutation_mapping_app {X: Type} :
forall (u1 u2 v1 v2 base : list X), forall (u1 u2 v1 v2 base : list X),
Permutation_mapping (u1 ++ u2) (v1 ++ v2) base Permutation_mapping (u1 ++ u2) (v1 ++ v2) base
-> length u1 = length v1 -> -> length u1 = length v1 ->
@ -127,7 +127,7 @@ Proof.
Qed. Qed.
Lemma permutation_mapping_base_cons {X: Type} : Lemma Permutation_mapping_base_cons {X: Type} :
forall (u v base : list X) a, forall (u v base : list X) a,
Permutation_mapping u v base -> Permutation_mapping u v (a::base). Permutation_mapping u v base -> Permutation_mapping u v (a::base).
Proof. Proof.
@ -144,7 +144,7 @@ Proof.
Qed. Qed.
Lemma permutation_mapping_self {X: Type} : Lemma Permutation_mapping_self {X: Type} :
forall (u base : list X), incl u base -> Permutation_mapping u u base. forall (u base : list X), incl u base -> Permutation_mapping u u base.
Proof. Proof.
intro u. induction u; intro base; intro H; exists base. intro u. induction u; intro base; intro H; exists base.
@ -155,7 +155,7 @@ Proof.
Qed. Qed.
Lemma permutation_mapping_length {X: Type} : Lemma Permutation_mapping_length {X: Type} :
forall (u v base : list X), forall (u v base : list X),
Permutation_mapping u v base -> length u = length v. Permutation_mapping u v base -> length u = length v.
Proof. Proof.
@ -167,7 +167,7 @@ Proof.
Qed. Qed.
Lemma permutation_mapping_swap {X: Type} : Lemma Permutation_mapping_swap {X: Type} :
forall (u v base : list X), forall (u v base : list X),
Permutation_mapping u v base -> Permutation_mapping v u base. Permutation_mapping u v base -> Permutation_mapping v u base.
Proof. Proof.
@ -302,7 +302,7 @@ Qed.
Lemma permutation_mapping_base {X: Type} : Lemma Permutation_mapping_base {X: Type} :
forall (u v base p: list X), forall (u v base p: list X),
Permutation base p -> Permutation_mapping u v base Permutation base p -> Permutation_mapping u v base
-> Permutation_mapping u v p. -> Permutation_mapping u v p.