Wie können Fixpoint-Definitionen innerhalb von Beweisen in Coq angewendet werden?

Question

Ich habe Probleme zu verstehen, wie man einige der Dinge, die ich in Coq definiert habe, in Beweisen verwendet. Ich habe dieses Fragment der Definition und Funktionen:

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. 

ich etwas scheinbar leicht zu beweisen, müssen aber treffe ich zwei Probleme:

Lemma LongCompress (C : string)(n : nat): n >=1 -> Rules 
((RepString n 0) |= (s 0 E)). 
Proof. 
intros. 
induction n. 
inversion H. 
simpl. 
apply compress. 

Also hier bin Problem ein, erhalte ich:

"Unable to unify "Rules (s ?M1805 (s ?M1805 ?M1806) |= s ?M1805 ?M1806)" with 
"Rules (s 0 (RepString n 0) |- s 0 E)".'" 

Jetzt kann ich sehen, warum ich den Fehler, während technisch RepString n 0 die gleichen wie s 0 (s 0 (s 0(... s 0 E))) ist, kann ich einfach nicht den Weg finden coq, dass wissen zu lassen, habe ich versucht, messing mit apply compress with wie 10 verschiedene Dinge kann ich es immer noch nicht richtig machen. Ich muss es so etwas "entfalten" (natürlich funktioniert unfold nicht ...).

Ich habe keine Ideen mehr und würde mich sehr für Ihre Anregungen bedanken!

EDIT VON jetzt an.

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. 

Ich habe die Lemmata verallgemeinert, dass Anton Trunov half mir beweisen, aber jetzt habe ich in eine andere Wand stieß. Ich denke, das Problem könnte mit der Art und Weise beginnen, wie ich das Theorem selbst geschrieben habe, ich werde jede Idee zu schätzen wissen.

Answer 1

ich etwas ein wenig allgemeinere beweisen würde: für zwei beliebige nicht-leere Strings von Nullen s = 0000...0 und t = 00...0, wenn length s > length t, dann s |= t, dh

forall n m, 
    m <> 0 -> 
    n > m -> 
    Rules (RepString n 0 |= RepString m 0). 

ist hier ein Helfer Lemma:

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. 

Jetzt können wir leicht unsere beworbenen allgemeine Lemma beweisen:

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. 

Es ist leicht zu sehen, dass jede ausreichend lange Kette von Nullen kann 0 in den Singleton-string komprimiert werden:

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.