Here is an inductive type pc
that I am using in a mathematical theorem.
Inductive pc ( n : nat ) : Type :=
| pcs : forall ( m : nat ), m < n -> pc n
| pcm : pc n -> pc n -> pc n.
And another inductive type pc_tree
, which is basically a binary tree that contains one or more pc
s. pcts
is a leaf node constructor that contains a single pc
, and pctm
is an internal node constructor that contains multiple pc
s.
Inductive pc_tree : Type :=
| pcts : forall ( n : nat ), pc n -> pc_tree
| pctm : pc_tree -> pc_tree -> pc_tree.
And an inductively defined proposition contains
. contains n x t
means that the tree t
contains at least one ocurrence of x : pc n
.
Inductive contains ( n : nat ) ( x : pc n ) : pc_tree -> Prop :=
| contain0 : contains n x ( pcts n x )
| contain1 : forall ( t s : pc_tree ), contains n x t -> contains n x ( pctm t s )
| contain2 : forall ( t s : pc_tree ), contains n x t -> contains n x ( pctm s t ).
Now, the problematic lemma I need to prove:
Lemma contains_single_eq : forall ( n : nat ) ( x y : pc n ), contains n x ( pcts n y ) -> x = y.
What the lemma means is really simple: if a tree that has a single leaf node containing y : pc n
contains some x : pc n
, it follows that x = y
. I thought I should be able to prove this with a simple inversion
on contains
. So When I wrote
Lemma contains_single_eq : forall ( n : nat ) ( x y : pc n ), contains n x ( pcts n y ) -> x = y.
intros n x y H. inversion H.
I was expecting to get x = y
as an hypothesis in the context. Here's what I got instead:
1 subgoal
n : nat
x : pc n
y : pc n
H : contains n x (pcts n y)
H1 : existT (fun n : nat => pc n) n x = existT (fun n : nat => pc n) n y
====================================================================== (1/1)
x = y
H1
is quite different from what I expected. (I've never seen existT
before.) All I care about is that I prove contains_single_eq
, but I'm not sure how to use H1
for it, or whether it is usable at all.
Any thoughts?
{x : T & P x}
is a dependent sum likeT * P
is a nondependent sum.@existT T P x H : {x : T & P x}
like@pair T P x H : T * P
.exists x : T, P x
,{x : T | P x}
, and{x : T & P x}
are very similar. Use thePrint ex.
,Print sig.
, andPrint sigT.
commands. – user3551663