无法证明排列 属性
Fail to prove a permutation property
我创建了这个简单的类型：
Inductive implist : nat -> list nat -> Prop :=
| GSSingle : forall (n:nat), implist n [n]
| GSPairLeft : forall (a b n:nat) (l:list nat), implist n l -> implist n ([a]++[b]++l)
| GSPairRight : forall (a b n:nat) (l:list nat), implist n l -> implist n (l++[a]++[b]).
我试图证明这个置换引理：
Lemma permutImplist :
forall (n a b c:nat) (input:list nat), implist n ((a::b::c::input)) <-> implist n ((c::b::a::input)).
我在类型本身或列表上尝试过各种归纳原则，但总是以死胡同告终。
有人可以帮我做这个证明吗？
谢谢！！
这个谓词的归纳原理对于直接证明这一点用处不大。最好找到 implist 的替代公式来让你的证明通过：
From Coq Require Import List PeanoNat Lia.
Import ListNotations.
Inductive implist : nat -> list nat -> Prop :=
| GSSingle : forall (n:nat), implist n [n]
| GSPairLeft : forall (a b n:nat) (l:list nat), implist n l -> implist n ([a]++[b]++l)
| GSPairRight : forall (a b n:nat) (l:list nat), implist n l -> implist n (l++[a]++[b]).
Lemma implist_alt n l :
implist n l <->
exists l1 l2,
l = l1 ++ n :: l2 /\
Nat.even (length l1) = true /\
Nat.even (length l2) = true.
Proof.
split.
- intros H. induction H as [n|a b n l _ IH|a b n l _ IH].
+ exists [], []; intuition.
+ destruct IH as (l1 & l2 & -> & Hl1 & Hl2).
exists (a :: b :: l1), l2; intuition.
+ destruct IH as (l1 & l2 & -> & Hl1 & Hl2).
exists l1, (l2 ++ [a; b]). simpl.
rewrite <- app_assoc, app_length, Nat.add_comm.
intuition.
- intros (l1 & l2 & -> & Hl1 & Hl2).
assert (Hb1 : exists b, length l1 < b) by (exists (S (length l1)); lia).
destruct Hb1 as (b1 & Hb1).
assert (Hb2 : exists b, length l2 < b) by (exists (S (length l2)); lia).
destruct Hb2 as (b2 & Hb2).
revert l1 b2 l2 Hl1 Hl2 Hb1 Hb2.
induction (Nat.lt_wf_0 b1) as [b1 _ IH1].
intros [| x1 [| y1 l1]]; simpl; try easy.
+ intros b2 l2 _ Hl2 _. revert l2 Hl2.
induction (Nat.lt_wf_0 b2) as [b2 _ IH2].
induction l2 as [|x2 l2 _] using rev_ind.
* intros _ _. apply GSSingle.
* induction l2 as [|y2 l2 _] using rev_ind; simpl; try easy.
rewrite !app_length. simpl. rewrite <- Nat.add_assoc, Nat.add_comm. simpl.
intros Hl2 Hb2. rewrite <- app_assoc.
change (n :: l2 ++ [y2] ++ [x2]) with ((n::l2) ++ [y2] ++ [x2]).
apply GSPairRight. apply (IH2 (S (S (length l2)))); eauto; lia.
+ intros b2 l2 Hl1 Hl2 Hb1 Hb2.
apply (GSPairLeft x1 y1). apply (IH1 (S (S (length l1))) Hb1 _ b2); eauto.
Qed.
Lemma permutImplist_aux :
forall (n a b c:nat) (input:list nat), implist n ((a::b::c::input)) -> implist n ((c::b::a::input)).
Proof.
intros n a b c l (l1 & l2 & e & Hl1 & Hl2)%implist_alt.
destruct l1 as [|x l1]; simpl in *.
{ injection e as <- <-; simpl in *.
apply implist_alt. exists [c; b], l; intuition. }
destruct l1 as [|y l1]; simpl in *; try easy.
injection e as <- <- e.
destruct l1 as [|z l1]; simpl in *.
{ injection e as <- <-.
apply implist_alt. exists [], (b :: a :: l); intuition. }
destruct l1 as [|w l1]; simpl in *; try easy.
injection e as <- ->.
apply implist_alt. exists (c :: b :: a :: w :: l1), l2.
intuition.
Qed.
Lemma permutImplist :
forall (n a b c:nat) (input:list nat), implist n ((a::b::c::input)) <-> implist n ((c::b::a::input)).
Proof.
intros n a b c l; split; apply permutImplist_aux.
Qed.
如您所见，棘手的部分是 implist_alt 的相反方向。证明这一点的理想方法是对长度为偶数的列表采用归纳原理。由于我们没有这个，我改为对偶数列表的长度使用强归纳法，效果也很好。
根据关于偶数列表归纳原理的建议，我已经能够为反向部分生成一个更短的证明：
Lemma implist_alt' :
forall (n:nat) (l:list nat), implist n l <-> exists l1 l2, l = l1 ++ n::l2 /\ Nat.Even (length l1) /\ Nat.Even (length l2).
Proof.
split.
- intros H. induction H as [n|a b n l _ IH|a b n l _ IH].
+ exists [], []; intuition; simpl; now exists 0.
+ destruct IH as (l1 & l2 & -> & Hl1 & Hl2).
exists (a :: b :: l1), l2. intuition. simpl. now rewrite Nat.Even_succ_succ.
+ destruct IH as (l1 & l2 & -> & Hl1 & Hl2).
exists l1, (l2 ++ [a; b]). simpl.
rewrite <- app_assoc, app_length, Nat.add_comm.
intuition. simpl. now rewrite Nat.Even_succ_succ.
- intros (l1 & l2 & -> & Hl1 & Hl2).
induction l1 using list_pair_induction.
simpl. now apply (EvenImplist n l2).
simpl in Hl1. rewrite Nat.Even_succ_succ in Hl1. apply IHl1 in Hl1. revert Hl1. now apply (GSPairLeft a b n (l1++n::l2)).
simpl in Hl1. exfalso. now apply Even_1.
Qed.
它在列表中使用以下归纳原则：
Section list_pair_induction.
Variable P : list nat -> Prop.
Hypothesis Hnil : P nil.
Hypothesis Hddn : forall (l:list nat) (a b:nat) , P l -> P (a::b::l).
Theorem allEven : forall (xs:list nat), even (length xs) = true -> P xs.
Proof.
intro.
remember (length xs) as n eqn : Heqn.
revert n xs Heqn.
induction n as [n IH] using (well_founded_induction lt_wf).
destruct n as [|n].
now destruct xs.
destruct n as [|n].
intros; discriminate.
destruct xs as [|a xs].
intros; discriminate.
destruct xs as [|b xs].
intros; discriminate.
simpl.
intros H1 H2.
apply Hddn.
apply IH with (y := n); auto.
now injection H1.
Qed.
Theorem allEven' : forall (xs:list nat), Nat.Even (length xs) -> P xs.
Proof.
intro.
rewrite <- Nat.even_spec.
apply allEven.
Qed.
Hypothesis Hsingle : forall (n:nat), P (n::nil).
Theorem Hsingle2Hsing : (forall n:nat, P(n::nil) ) -> forall (xs:list nat), (1 = length xs) -> P xs.
Proof.
induction xs.
intro.
exfalso.
simpl in H0.
congruence.
induction xs.
intro.
apply Hsingle.
intro.
exfalso.
simpl in H0.
congruence.
Qed.
Theorem allOdd : forall (xs:list nat), odd (length xs) = true -> P xs.
Proof.
intro.
remember (length xs) as n eqn : Heqn.
revert n xs Heqn.
induction n as [n IH] using (well_founded_induction lt_wf).
destruct n as [|n].
now destruct xs.
destruct n as [|n].
intros.
generalize Heqn.
generalize xs.
generalize Hsingle.
apply Hsingle2Hsing.
destruct xs as [|a xs].
intros; discriminate.
destruct xs as [|b xs].
intros; discriminate.
simpl.
intros H1 H2.
apply Hddn.
apply IH with (y := n); auto.
now injection H1.
Qed.
Hypothesis Hsing : forall (l:list nat) , (1 = length l) -> P (l).
Theorem allOddsing : forall (xs:list nat), odd (length xs) = true -> P xs.
Proof.
intro.
remember (length xs) as n eqn : Heqn.
revert n xs Heqn.
induction n as [n IH] using (well_founded_induction lt_wf).
destruct n as [|n].
now destruct xs.
destruct n as [|n].
intros.
apply Hsing.
assumption.
destruct xs as [|a xs].
intros; discriminate.
destruct xs as [|b xs].
intros; discriminate.
simpl.
intros H1 H2.
apply Hddn.
apply IH with (y := n); auto.
now injection H1.
Qed.
Theorem allOdd' : forall (xs:list nat), Nat.Odd (length xs) -> P xs.
Proof.
intro.
rewrite <- Nat.odd_spec.
apply allOdd.
Qed.
Theorem list_pair_induction : forall (xs:list nat), P xs.
Proof.
intro.
remember (length xs) as n eqn : Heqn.
destruct even_odd_dec with n.
apply allEven'.
rewrite <- Heqn.
assumption.
apply allOdd'.
rewrite <- Heqn.
assumption.
Qed.
End list_pair_induction.
我创建了这个简单的类型：
Inductive implist : nat -> list nat -> Prop :=
| GSSingle : forall (n:nat), implist n [n]
| GSPairLeft : forall (a b n:nat) (l:list nat), implist n l -> implist n ([a]++[b]++l)
| GSPairRight : forall (a b n:nat) (l:list nat), implist n l -> implist n (l++[a]++[b]).
我试图证明这个置换引理：
Lemma permutImplist :
forall (n a b c:nat) (input:list nat), implist n ((a::b::c::input)) <-> implist n ((c::b::a::input)).
我在类型本身或列表上尝试过各种归纳原则，但总是以死胡同告终。
有人可以帮我做这个证明吗？
谢谢！！
这个谓词的归纳原理对于直接证明这一点用处不大。最好找到 implist 的替代公式来让你的证明通过：
From Coq Require Import List PeanoNat Lia.
Import ListNotations.
Inductive implist : nat -> list nat -> Prop :=
| GSSingle : forall (n:nat), implist n [n]
| GSPairLeft : forall (a b n:nat) (l:list nat), implist n l -> implist n ([a]++[b]++l)
| GSPairRight : forall (a b n:nat) (l:list nat), implist n l -> implist n (l++[a]++[b]).
Lemma implist_alt n l :
implist n l <->
exists l1 l2,
l = l1 ++ n :: l2 /\
Nat.even (length l1) = true /\
Nat.even (length l2) = true.
Proof.
split.
- intros H. induction H as [n|a b n l _ IH|a b n l _ IH].
+ exists [], []; intuition.
+ destruct IH as (l1 & l2 & -> & Hl1 & Hl2).
exists (a :: b :: l1), l2; intuition.
+ destruct IH as (l1 & l2 & -> & Hl1 & Hl2).
exists l1, (l2 ++ [a; b]). simpl.
rewrite <- app_assoc, app_length, Nat.add_comm.
intuition.
- intros (l1 & l2 & -> & Hl1 & Hl2).
assert (Hb1 : exists b, length l1 < b) by (exists (S (length l1)); lia).
destruct Hb1 as (b1 & Hb1).
assert (Hb2 : exists b, length l2 < b) by (exists (S (length l2)); lia).
destruct Hb2 as (b2 & Hb2).
revert l1 b2 l2 Hl1 Hl2 Hb1 Hb2.
induction (Nat.lt_wf_0 b1) as [b1 _ IH1].
intros [| x1 [| y1 l1]]; simpl; try easy.
+ intros b2 l2 _ Hl2 _. revert l2 Hl2.
induction (Nat.lt_wf_0 b2) as [b2 _ IH2].
induction l2 as [|x2 l2 _] using rev_ind.
* intros _ _. apply GSSingle.
* induction l2 as [|y2 l2 _] using rev_ind; simpl; try easy.
rewrite !app_length. simpl. rewrite <- Nat.add_assoc, Nat.add_comm. simpl.
intros Hl2 Hb2. rewrite <- app_assoc.
change (n :: l2 ++ [y2] ++ [x2]) with ((n::l2) ++ [y2] ++ [x2]).
apply GSPairRight. apply (IH2 (S (S (length l2)))); eauto; lia.
+ intros b2 l2 Hl1 Hl2 Hb1 Hb2.
apply (GSPairLeft x1 y1). apply (IH1 (S (S (length l1))) Hb1 _ b2); eauto.
Qed.
Lemma permutImplist_aux :
forall (n a b c:nat) (input:list nat), implist n ((a::b::c::input)) -> implist n ((c::b::a::input)).
Proof.
intros n a b c l (l1 & l2 & e & Hl1 & Hl2)%implist_alt.
destruct l1 as [|x l1]; simpl in *.
{ injection e as <- <-; simpl in *.
apply implist_alt. exists [c; b], l; intuition. }
destruct l1 as [|y l1]; simpl in *; try easy.
injection e as <- <- e.
destruct l1 as [|z l1]; simpl in *.
{ injection e as <- <-.
apply implist_alt. exists [], (b :: a :: l); intuition. }
destruct l1 as [|w l1]; simpl in *; try easy.
injection e as <- ->.
apply implist_alt. exists (c :: b :: a :: w :: l1), l2.
intuition.
Qed.
Lemma permutImplist :
forall (n a b c:nat) (input:list nat), implist n ((a::b::c::input)) <-> implist n ((c::b::a::input)).
Proof.
intros n a b c l; split; apply permutImplist_aux.
Qed.
如您所见，棘手的部分是 implist_alt 的相反方向。证明这一点的理想方法是对长度为偶数的列表采用归纳原理。由于我们没有这个，我改为对偶数列表的长度使用强归纳法，效果也很好。
根据关于偶数列表归纳原理的建议，我已经能够为反向部分生成一个更短的证明：
Lemma implist_alt' :
forall (n:nat) (l:list nat), implist n l <-> exists l1 l2, l = l1 ++ n::l2 /\ Nat.Even (length l1) /\ Nat.Even (length l2).
Proof.
split.
- intros H. induction H as [n|a b n l _ IH|a b n l _ IH].
+ exists [], []; intuition; simpl; now exists 0.
+ destruct IH as (l1 & l2 & -> & Hl1 & Hl2).
exists (a :: b :: l1), l2. intuition. simpl. now rewrite Nat.Even_succ_succ.
+ destruct IH as (l1 & l2 & -> & Hl1 & Hl2).
exists l1, (l2 ++ [a; b]). simpl.
rewrite <- app_assoc, app_length, Nat.add_comm.
intuition. simpl. now rewrite Nat.Even_succ_succ.
- intros (l1 & l2 & -> & Hl1 & Hl2).
induction l1 using list_pair_induction.
simpl. now apply (EvenImplist n l2).
simpl in Hl1. rewrite Nat.Even_succ_succ in Hl1. apply IHl1 in Hl1. revert Hl1. now apply (GSPairLeft a b n (l1++n::l2)).
simpl in Hl1. exfalso. now apply Even_1.
Qed.
它在列表中使用以下归纳原则：
Section list_pair_induction.
Variable P : list nat -> Prop.
Hypothesis Hnil : P nil.
Hypothesis Hddn : forall (l:list nat) (a b:nat) , P l -> P (a::b::l).
Theorem allEven : forall (xs:list nat), even (length xs) = true -> P xs.
Proof.
intro.
remember (length xs) as n eqn : Heqn.
revert n xs Heqn.
induction n as [n IH] using (well_founded_induction lt_wf).
destruct n as [|n].
now destruct xs.
destruct n as [|n].
intros; discriminate.
destruct xs as [|a xs].
intros; discriminate.
destruct xs as [|b xs].
intros; discriminate.
simpl.
intros H1 H2.
apply Hddn.
apply IH with (y := n); auto.
now injection H1.
Qed.
Theorem allEven' : forall (xs:list nat), Nat.Even (length xs) -> P xs.
Proof.
intro.
rewrite <- Nat.even_spec.
apply allEven.
Qed.
Hypothesis Hsingle : forall (n:nat), P (n::nil).
Theorem Hsingle2Hsing : (forall n:nat, P(n::nil) ) -> forall (xs:list nat), (1 = length xs) -> P xs.
Proof.
induction xs.
intro.
exfalso.
simpl in H0.
congruence.
induction xs.
intro.
apply Hsingle.
intro.
exfalso.
simpl in H0.
congruence.
Qed.
Theorem allOdd : forall (xs:list nat), odd (length xs) = true -> P xs.
Proof.
intro.
remember (length xs) as n eqn : Heqn.
revert n xs Heqn.
induction n as [n IH] using (well_founded_induction lt_wf).
destruct n as [|n].
now destruct xs.
destruct n as [|n].
intros.
generalize Heqn.
generalize xs.
generalize Hsingle.
apply Hsingle2Hsing.
destruct xs as [|a xs].
intros; discriminate.
destruct xs as [|b xs].
intros; discriminate.
simpl.
intros H1 H2.
apply Hddn.
apply IH with (y := n); auto.
now injection H1.
Qed.
Hypothesis Hsing : forall (l:list nat) , (1 = length l) -> P (l).
Theorem allOddsing : forall (xs:list nat), odd (length xs) = true -> P xs.
Proof.
intro.
remember (length xs) as n eqn : Heqn.
revert n xs Heqn.
induction n as [n IH] using (well_founded_induction lt_wf).
destruct n as [|n].
now destruct xs.
destruct n as [|n].
intros.
apply Hsing.
assumption.
destruct xs as [|a xs].
intros; discriminate.
destruct xs as [|b xs].
intros; discriminate.
simpl.
intros H1 H2.
apply Hddn.
apply IH with (y := n); auto.
now injection H1.
Qed.
Theorem allOdd' : forall (xs:list nat), Nat.Odd (length xs) -> P xs.
Proof.
intro.
rewrite <- Nat.odd_spec.
apply allOdd.
Qed.
Theorem list_pair_induction : forall (xs:list nat), P xs.
Proof.
intro.
remember (length xs) as n eqn : Heqn.
destruct even_odd_dec with n.
apply allEven'.
rewrite <- Heqn.
assumption.
apply allOdd'.
rewrite <- Heqn.
assumption.
Qed.
End list_pair_induction.