如何在 Coq 的证明中应用 Fixpoint 定义?
How to apply Fixpoint definitions within proofs in Coq?
我无法理解如何在证明中使用我在 Coq 中定义的一些东西。我有这个定义和函数片段:
Inductive string : Set :=
| E : string
| s : nat -> string -> string.
Inductive deduce : Set :=
|de : string -> string -> deduce.
Infix "|=" := de.
Inductive Rules : deduce -> Prop :=
| compress : forall (n : nat) (A : string), rule (( s n ( s n A)) |= ( s n A))
| transitive : forall A B C : string, rule (A |= B) -> rule (B |= C) -> rule (A |= C).
Fixpoint RepString (n m : nat): string:=
match n with
|0 => E
|S n => s m ( RepString n m)
end.
我需要证明一些看似简单的事情,但我遇到了两个问题:
Lemma LongCompress (C : string)(n : nat): n >=1 -> Rules
((RepString n 0 ) |= (s 0 E) ).
Proof.
intros.
induction n.
inversion H.
simpl.
apply compress.
所以这里我有问题一,我得到:
"Unable to unify "Rules (s ?M1805 (s ?M1805 ?M1806) |= s ?M1805 ?M1806)" with
"Rules (s 0 (RepString n 0) |- s 0 E)".'"
现在,我明白了为什么会出现错误,而从技术上讲 RepString n 0
与 s 0 (s 0 (s 0( ... s 0 E)))
相同,我只是找不到让 coq 知道的方法,我试过了弄乱 apply compress with
就像 10 种不同的东西,我仍然无法正确处理。我需要 "unfold" 类似的东西(当然 unfold
不起作用...)。
我没有想法,非常感谢您对此的任何意见!
从现在开始编辑。
Inductive Rules : deduce -> Prop :=
| compress : forall (n : nat) (A : string), rule (( s n ( s n A)) |= ( s n A))
| transitive : forall A B C : string, rule (A |= B) -> rule (B |= C) -> rule (A |= C)
| inspection : forall (n m : nat) (A : string), m < n -> rule ((s n A) |- (s m A)).
Definition less (n :nat ) (A B : string) := B |= (s n A).
Lemma oneLess (n m : nat): rule (less 0 (RepString n 1) (RepString m 1)) <-> n< m.
我已经概括了 Anton Trunov 帮助我证明的引理,但现在我碰到了另一堵墙。我认为问题可能始于我编写定理本身的方式,我会很感激任何想法。
我会证明一些更一般的东西:对于任意两个非空的零字符串 s = 0000...0
和 t = 00...0
,如果 length s > length t
,则 s |= t
,即
forall n m,
m <> 0 ->
n > m ->
Rules (RepString n 0 |= RepString m 0).
这是一个辅助引理:
Require Import Coq.Arith.Arith.
Require Import Coq.omega.Omega.
Hint Constructors Rules. (* add this line after the definition of `Rules` *)
Lemma LongCompress_helper (n m k : nat):
n = (S m) + k ->
Rules (RepString (S n) 0 |= RepString (S m) 0).
Proof.
generalize dependent m.
generalize dependent n.
induction k; intros n m H.
- Search (?X + 0 = ?X). rewrite Nat.add_0_r in H.
subst. simpl. eauto.
- apply (transitive _ (RepString n 0) _); simpl in H; rewrite H.
+ simpl. constructor.
+ apply IHk. omega.
Qed.
现在,我们可以很容易地证明我们所宣传的一般引理:
Lemma LongCompress_general (n m : nat):
m <> 0 ->
n > m ->
Rules (RepString n 0 |= RepString m 0).
Proof.
intros Hm Hn. destruct n.
- inversion Hn.
- destruct m.
+ exfalso. now apply Hm.
+ apply LongCompress_helper with (k := n - m - 1). omega.
Qed.
很容易看出任何足够长的零串都可以压缩成单例串 0
:
Lemma LongCompress (n : nat):
n > 1 -> Rules ( RepString n 0 |= s 0 E ).
Proof.
intro H. replace (s 0 E) with (RepString 1 0) by easy.
apply LongCompress_general; auto.
Qed.
我无法理解如何在证明中使用我在 Coq 中定义的一些东西。我有这个定义和函数片段:
Inductive string : Set :=
| E : string
| s : nat -> string -> string.
Inductive deduce : Set :=
|de : string -> string -> deduce.
Infix "|=" := de.
Inductive Rules : deduce -> Prop :=
| compress : forall (n : nat) (A : string), rule (( s n ( s n A)) |= ( s n A))
| transitive : forall A B C : string, rule (A |= B) -> rule (B |= C) -> rule (A |= C).
Fixpoint RepString (n m : nat): string:=
match n with
|0 => E
|S n => s m ( RepString n m)
end.
我需要证明一些看似简单的事情,但我遇到了两个问题:
Lemma LongCompress (C : string)(n : nat): n >=1 -> Rules
((RepString n 0 ) |= (s 0 E) ).
Proof.
intros.
induction n.
inversion H.
simpl.
apply compress.
所以这里我有问题一,我得到:
"Unable to unify "Rules (s ?M1805 (s ?M1805 ?M1806) |= s ?M1805 ?M1806)" with
"Rules (s 0 (RepString n 0) |- s 0 E)".'"
现在,我明白了为什么会出现错误,而从技术上讲 RepString n 0
与 s 0 (s 0 (s 0( ... s 0 E)))
相同,我只是找不到让 coq 知道的方法,我试过了弄乱 apply compress with
就像 10 种不同的东西,我仍然无法正确处理。我需要 "unfold" 类似的东西(当然 unfold
不起作用...)。
我没有想法,非常感谢您对此的任何意见!
从现在开始编辑。
Inductive Rules : deduce -> Prop :=
| compress : forall (n : nat) (A : string), rule (( s n ( s n A)) |= ( s n A))
| transitive : forall A B C : string, rule (A |= B) -> rule (B |= C) -> rule (A |= C)
| inspection : forall (n m : nat) (A : string), m < n -> rule ((s n A) |- (s m A)).
Definition less (n :nat ) (A B : string) := B |= (s n A).
Lemma oneLess (n m : nat): rule (less 0 (RepString n 1) (RepString m 1)) <-> n< m.
我已经概括了 Anton Trunov 帮助我证明的引理,但现在我碰到了另一堵墙。我认为问题可能始于我编写定理本身的方式,我会很感激任何想法。
我会证明一些更一般的东西:对于任意两个非空的零字符串 s = 0000...0
和 t = 00...0
,如果 length s > length t
,则 s |= t
,即
forall n m,
m <> 0 ->
n > m ->
Rules (RepString n 0 |= RepString m 0).
这是一个辅助引理:
Require Import Coq.Arith.Arith.
Require Import Coq.omega.Omega.
Hint Constructors Rules. (* add this line after the definition of `Rules` *)
Lemma LongCompress_helper (n m k : nat):
n = (S m) + k ->
Rules (RepString (S n) 0 |= RepString (S m) 0).
Proof.
generalize dependent m.
generalize dependent n.
induction k; intros n m H.
- Search (?X + 0 = ?X). rewrite Nat.add_0_r in H.
subst. simpl. eauto.
- apply (transitive _ (RepString n 0) _); simpl in H; rewrite H.
+ simpl. constructor.
+ apply IHk. omega.
Qed.
现在,我们可以很容易地证明我们所宣传的一般引理:
Lemma LongCompress_general (n m : nat):
m <> 0 ->
n > m ->
Rules (RepString n 0 |= RepString m 0).
Proof.
intros Hm Hn. destruct n.
- inversion Hn.
- destruct m.
+ exfalso. now apply Hm.
+ apply LongCompress_helper with (k := n - m - 1). omega.
Qed.
很容易看出任何足够长的零串都可以压缩成单例串 0
:
Lemma LongCompress (n : nat):
n > 1 -> Rules ( RepString n 0 |= s 0 E ).
Proof.
intro H. replace (s 0 E) with (RepString 1 0) by easy.
apply LongCompress_general; auto.
Qed.