Consider following mutual inductive proposition
Inductive TypeA : Prop :=
| ConstructorA : TypeB -> TypeA
with TypeB : Prop :=
| ConstructorB : TypeA -> TypeB.
Here is proof of ~TypeA in functional style
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
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.
Edit: Found that Coq have such syntax for mutual theorems but it throws error
Lemma TypeA_is_empty : ~ TypeA
with TypeB_is_empty : ~ TypeB.
**Cannot find common (mutual) inductive premises or coinductive conclusions in the statements.**
(I have changed names around for convenience.)
First of all, you cannot use not in the statement, this one compiles:
Lemma A_is_empty : A -> False
with B_is_empty : B -> False.
That said, this code seems to do it. See the comments for the explanation:
Inductive A : Prop :=
| mkA : B -> A
with B : Prop :=
| mkB : A -> B.
Fixpoint A_is_empty' (a : A) : False :=
match a with
| mkA b => B_is_empty' b
end
with B_is_empty' (b : B) : False :=
match b with
| mkB a => A_is_empty' a
end.
Lemma A_is_empty : A -> False
with B_is_empty : B -> False.
Proof.
- intros a.
apply A_is_empty.
exact a.
- intros b.
apply B_is_empty.
exact b.
Fail Qed. (* Recursive call to A_is_empty
has principal argument equal to
"a" instead of a subterm of "a". *)
Abort.
Lemma A_is_empty : A -> False
with B_is_empty : B -> False.
Proof.
- intros a.
destruct a as [b]. (* !! *)
apply B_is_empty.
exact b.
- intros b.
destruct b as [a]. (* !! *)
apply A_is_empty.
exact a.
Qed.
Check A_is_empty : ~ A.
Check B_is_empty : ~ B.