Coq 归纳形式不正确

Question

我因 IH 结构不完善而遇到麻烦（或者我犯了错误）。

From stdpp Require Import mapset.

From stdpp Require Import gmap.
From stdpp Require Import options.
From stdpp Require Import proofmode.
From iris.heap_lang Require Export proofmode notation.

Definition Node : Type := nat.
Definition Children : Type := (loc * loc).
Definition Entry : Type := (Node * Children).

Definition ldd_state : Type := gmap loc (nat * (loc * loc)).

Definition ldd_zero : loc := Loc 0.
Definition ldd_one : loc := Loc 1.

(* Loc 0 and Loc 1 will never be present in the state.
   This is to prevent the true, false leaves having children and values. *)
Definition state_ok (ls : ldd_state) : Prop :=
  ls !! ldd_zero = None ∧ ls !! ldd_one = None.
    
Definition get_down (ls : ldd_state) (x : loc) : option loc := 
  ls !! x ≫= λ n, Some (snd n) ≫= λ n, Some (fst n).

Definition path := list loc.
Identity Coercion path_to_list : path >-> list.

Inductive valid_path (ls : ldd_state) (x : loc) : path → Prop :=
  | path_Et : x = ldd_one → valid_path ls x [ldd_one]
  | path_D  : ∀ (xd : loc) (p' : path),
      get_down ls x = Some xd → 
      valid_path ls xd p' → 
      valid_path ls x (x :: p').

Lemma path_equal : ∀ (ls : ldd_state) (x : loc) (p p' : path),
  state_ok ls → valid_path ls x p → valid_path ls x p' → p = p'.
intros. induction H0.
Proof.
- destruct H1.  + admit. (* easy case, this is contradiction *)
                + admit. (* again, easy contradiction *)
- destruct H1.  + admit. (* easy case, contradiction *)
                + (* Stuck here *)
 Admitted.

查看 IH 时，没有考虑到之前的路径，通过沿着

down

边缘，会将

x

从

x::p'

中“移除”，以及应该是

p'0 = p' 的结果

.

目前：

IHvalid_path : valid_path ls xd (x :: p') → p'0 = x :: p'

我需要什么：

IHvalid_path : valid_path ls xd p'0 → valid_path ls xd p' → p'0 = p'

我尝试过多种方法，例如概括。但我似乎无法弄清楚这一点。谢谢！

Answer 1

您可以通过将假设转化为目标来“概括归纳假设”。

revert