Consider following mutual inductive proposition
<code>Inductive TypeA : Prop :=
| ConstructorA : TypeB -> TypeA
with TypeB : Prop :=
| ConstructorB : TypeA -> TypeB.
</code>
<code>Inductive TypeA : Prop :=
| ConstructorA : TypeB -> TypeA
with TypeB : Prop :=
| ConstructorB : TypeA -> TypeB.
</code>
Inductive TypeA : Prop :=
| ConstructorA : TypeB -> TypeA
with TypeB : Prop :=
| ConstructorB : TypeA -> TypeB.
Here is proof of ~TypeA in functional style
<code>Fixpoint TypeA_is_empty' (a : TypeA) : False :=
match a with
| ConstructorA b' => TypeB_is_empty' b'
end
with TypeB_is_empty' (b : TypeB) : False :=
match b with
| ConstructorB a' => TypeA_is_empty' a'
end.
</code>
<code>Fixpoint TypeA_is_empty' (a : TypeA) : False :=
match a with
| ConstructorA b' => TypeB_is_empty' b'
end
with TypeB_is_empty' (b : TypeB) : False :=
match b with
| ConstructorB a' => TypeA_is_empty' a'
end.
</code>
Fixpoint TypeA_is_empty' (a : TypeA) : False :=
match a with
| ConstructorA b' => TypeB_is_empty' b'
end
with TypeB_is_empty' (b : TypeB) : False :=
match b with
| ConstructorB a' => TypeA_is_empty' a'
end.
How to prove ~TypeA in tactic style?
I want to be able to prove them as mutual Theorems if something similar exists in Coq
<code>Theorem TypeA_is_empty : ~ TypeA.
Theorem TypeB_is_empty : ~ TypeB.
Proof.
unfold not.
intros b.
inversion b as [a].
apply (TypeA_is_empty a).
Qed.
Proof.
unfold not.
intros a.
inversion a as [b].
apply (TypeB_is_empty b).
Qed.
</code>
<code>Theorem TypeA_is_empty : ~ TypeA.
Theorem TypeB_is_empty : ~ TypeB.
Proof.
unfold not.
intros b.
inversion b as [a].
apply (TypeA_is_empty a).
Qed.
Proof.
unfold not.
intros a.
inversion a as [b].
apply (TypeB_is_empty b).
Qed.
</code>
Theorem TypeA_is_empty : ~ TypeA.
Theorem TypeB_is_empty : ~ TypeB.
Proof.
unfold not.
intros b.
inversion b as [a].
apply (TypeA_is_empty a).
Qed.
Proof.
unfold not.
intros a.
inversion a as [b].
apply (TypeB_is_empty b).
Qed.