Induktion über Beziehungen

Question

Ich versuche, den folgende Spielzeug Satz über die Ordnung des Naturals zu beweisen:

Inductive Le: nat -> nat -> Prop := 
    | le_n: forall n, Le n n 
    | le_S: forall n m, Le n m -> Le n (S m). 

Theorem le_Sn_m: forall n m, 
    Le (S n) m -> Le n m. 

Auf dem Papier ist dies eine einfache Induktion über Le (S n) m. Insbesondere ist der Basisfall le_n trivial. obwohl

In Coq, meinen Beweis mit Induktion Anfang gibt mir folgend:

Proof. 
    intros n m H. induction H. 

1 subgoal 
n, n0 : nat 
______________________________________(1/1) 
Le n n0 

... in dem Fall, dass ich gesperrt bin.

Wie soll ich stattdessen verfahren?

Answer 1

Dies geschieht, weil Coq anders Indizes behandelt und Parameter (siehe akzeptierte Antwort auf this question für eine sehr schöne Erklärung). Ihre Le Beziehung verwendet Indizes nur, während die Standard-Definition das erste Argument ein Parameter macht:

Inductive le (n : nat) : nat -> Prop := 
| le_n : n <= n 
| le_S : forall m : nat, n <= m -> n <= S m 

ich empfehlen kann this blog post von James Wilcox zu lesen. Hier ist ein relevanter Auszug:

Wenn Coq eine Fallanalyse durchführt, abstrahiert es zunächst über alle Indizes. Möglicherweise haben Sie dieses Manifest als Informationsverlust gesehen, wenn auf Prädikate

So Destruct verwenden, können Sie entweder (1) Ihre Le Beziehung ändern, damit es einen Parameter verwenden würde, oder (2) die remember Taktik wie war von @Zimm I48 vorgeschlagen, oder (3) die dependent induction Taktik von @Vinz erwähnt:

Require Import Coq.Program.Equality. (* for `dependent induction` *) 

Inductive Le: nat -> nat -> Prop := 
    | le_n: forall n, Le n n 
    | le_S: forall n m, Le n m -> Le n (S m). 
Hint Constructors Le.     (* so `auto` will work *) 

Theorem le_Sn_m: forall n m, 
    Le (S n) m -> Le n m. 
Proof. intros n m H. dependent induction H; auto. Qed. 

Answer 2

Dies ist aufgrund einer Beschränkung von Coq, wenn induction auf Begriff, die nicht nur Variablen verwendet werden. Indem Sie Ihre Induktion machen, vergisst Coq die Tatsache, dass das erste Argument ein S von einigen n war.

Sie können stattdessen folgendes tun:

Theorem le_Sn_m_: forall X m, 
    Le X m -> forall n, X = S n -> Le n m. 

Ich denke, es gibt dependent induction irgendwo ist, dass Sie diese Zwischen Lemma retten könnte, aber ich kann mich nicht erinnern, wo.

Answer 3

ähnlich @Vinz Vorschlag, aber ohne die Aussage zu ändern Sie beweisen:

Proof. 
    intros n m H. 
    remember (S n) as p. 
    induction H. 

die remember Taktik wird eine Gleichheit in Ihrem Kontext einzuführen, die diese kritischen Informationen zu verlieren werden vermieden.