I have troubles with a not well formed IH (or I am making mistakes).
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.
When viewing the IH, it does not take into consideration that that the previous path, by following the down edge, would "remove" the x from x::p', as well as the result that should have been p'0 = p'.
Currently:
IHvalid_path : valid_path ls xd (x :: p') → p'0 = x :: p'
What I need:
IHvalid_path : valid_path ls xd p'0 → valid_path ls xd p' → p'0 = p'
I have tried multiple things, such as generalize. But I cannot seem to figure this out. Thanks!
You can "generalize the induction hypothesis" by reverting assumptions into the goal.
(* instead of induction H0 *)
revert p' H1; induction H0.