Stream: Coq users

Topic: ✔ Why variable is not substituted?


view this post on Zulip lengyijun (Aug 02 2022 at 13:07):

A beginner's question:

Require Import
  Coq.Lists.List
  PeanoNat
  Lia.

Inductive u8 : Set :=
  | u8_cons : nat -> u8.

Inductive immut_u8_bw : Set :=
  | immut_u8_bw_cons : nat -> immut_u8_bw.


Inductive origin : Set :=
  | origin_cons : nat -> origin.


Inductive mir : Set :=
  | borrow_immut (x : immut_u8_bw) (y : u8).

Inductive mark_as_loan_origin : list mir -> origin -> Prop :=
  | borrow_immut_mark_as_loan_origin : forall l i (x : immut_u8_bw)(y : u8),
                                       Some(borrow_immut x y) = nth_error l i
                                    -> mark_as_loan_origin l (origin_cons (length l + i)).


Lemma loan_larger_length : forall l o,
                           mark_as_loan_origin l (origin_cons o)
                        -> o >= length l.
Proof.
intros.
generalize H; intros.
destruct H.
(* stuck here *)
(* Why o is not substituted in the goal ? *)

view this post on Zulip Gaëtan Gilbert (Aug 02 2022 at 13:15):

why would it be?

view this post on Zulip James Wood (Aug 03 2022 at 08:43):

Is it that you want something like inversion, dependent destruction, or dependent elimination (from Equations)?

view this post on Zulip Notification Bot (Aug 03 2022 at 11:30):

lengyijun has marked this topic as resolved.

view this post on Zulip lengyijun (Aug 03 2022 at 11:31):

@James Wood Thx


Last updated: Sep 26 2023 at 12:02 UTC