2
$\begingroup$

I'm working on developing a theory of arithmetic within a framework for first-order logic I constructed in Coq. The following is a simplified version of the scenario I'm working with.

Inductive Sigma' : nat -> arith_formula -> Prop :=
  | sigma_pi' n f : Pi' n f -> Sigma' (S n) f
  | sigma_exis' n x f : Sigma' (S n) f -> Sigma' (S n) (fexis x f)
with Pi' : nat -> arith_formula -> Prop :=
  | pi_sigma' n f : Sigma' n f -> Pi' (S n) f
  | pi_univ' n x f : Pi' (S n) f -> Pi' (S n) (funiv x f).

Lemma Sigma_n_ind' n : forall (P : forall f, Sigma' (S n) f -> Prop),
  (forall f (H:Pi' n f), P f (sigma_pi' _ f H)) ->
  (forall x f (H:Sigma' (S n) f), P f H -> P (fexis x f) (sigma_exis' _ x f H)) ->
  forall f (H:Sigma' (S n) f), P f H.
Proof.
  intros P Hpi Hexis.
  refine (fix Sigma_n_ind' f H {struct H} := _).
  dependent destruction H; [> apply Hpi | apply Hexis];
    apply Sigma_n_ind'.
Qed.

In the full version, these inductive definitions have more cases, but this should suffice to find a solution.

The problem is that this lemma uses a dependent destruction, which causes it to use Eqdep.Eq_rect_eq.eq_rect_eq as an axiom. I would really like to avoid invoking any axioms at all. I've tried unfolding the generated proof, but the proof of JMeq_eq doesn't seem to work for a particular case such as forall (x y : Sigma n f), x ~= y -> x = y.

And, no, induction does not work on H. I get:

Abstracting over the terms "n0" and "f" leads to a term
fun (n1 : nat) (f0 : arith_formula) =>
forall P0 : forall f1 : arith_formula, Sigma' n1 f1 -> Prop,
(forall (f1 : arith_formula) (H0 : Pi' n f1), P0 f1 (sigma_pi' n f1 H0)) ->
(forall (x : variable) (f1 : arith_formula) (H0 : Sigma' n1 f1),
 P0 f1 H0 -> P0 (fexis x f1) (sigma_exis' n x f1 H0)) -> P0 f0 H
which is ill-typed.
Reason is: Illegal application: 
The term "P0" of type "forall f : arith_formula, Sigma' n1 f -> Prop"
cannot be applied to the terms
 "f1" : "arith_formula"
 "sigma_pi' n f1 H0" : "Sigma' (S n) f1"
The 2nd term has type "Sigma' (S n) f1" which should be coercible to 
"Sigma' n1 f1".

Is there any way to complete this proof without invoking this axiom?

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ I don't have enough brainpower to flesh this out but IIUC yes you can prove this in theory without the axiom, because no variable in the index appears twice, and assuming arith_formula is an inductive type and fexis etc are constructors, everything is in order for pattern matching without K. How to efficiently do that in practice though I do not have enough expertise to say. $\endgroup$
    – Trebor ♦
    Commented Sep 5, 2023 at 16:37
  • $\begingroup$ Are you aware of Scheme and Combined Scheme to generate mutual induction principles? In your case, I'm not sure what the exact solution should be, because as it is both your inductive predicates are empty (since you are missing a base case). But I would advise you to use Combined Scheme to generate a mutual induction principle, together with a possible fiddling with remember to turn the S n index into a generic variable + an equality proof. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Sep 5, 2023 at 17:38
  • 1
    $\begingroup$ Another remark: dependently-typed induction principles on propositions (like the one you are trying to prove) are in general useless. This is because of proof irrelevance, which implies that it is impossible to define a function P : forall f, (H : Sigma f (S n)) -> Prop which is not constant in its second argument. Thus, it is probably enough to prove a non-dependent induction principle, ie one with P : arith_formula -> Type. Note that this is why by default Coq does not generate a dependent induction principle for propositions. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Sep 5, 2023 at 17:41
  • $\begingroup$ @MevenLennon-Bertrand Thank you! I'd already tried Scheme, which didn't work, but combining remember and using P : arith_formula -> Prop worked perfectly! The base case, by the way, is quantifier_free f -> Sigma 0 f and likewise for Pi 0 f, but that is its own inductive definition, which I felt would overcomplicate the problem. $\endgroup$
    – Circuit Craft
    Commented Sep 5, 2023 at 21:22
  • $\begingroup$ I figured it would be something like this, and I think that, just like arith_formula, having it around as a black-box constant would make the inductive look more like what you are interested in. But anyway, since you've solved your problem that's irrelevant. Maybe you could self-answer your question though, outlining the main steps that unlocked you? That's good SE practice, so that others finding your question when faced with similar issues can solve theirs too. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Sep 6, 2023 at 8:55

1 Answer 1

Reset to default
2
$\begingroup$

Thanks to @MevenLennon-Bertrand for suggesting this solution.

The following is an expanded form of the definitions, more similar to how they appear in my codebase.

Inductive Sigma : nat -> arith_formula -> Prop :=
  | sigma_qf f : quantifier_free f -> Sigma 0 f
  | sigma_pi n f : Pi n f -> Sigma (S n) f
  | sigma_exis n x f : Sigma (S n) f -> Sigma (S n) (fexis x f)
with Pi : nat -> arith_formula -> Prop :=
  | pi_qf f : quantifier_free f -> Pi 0 f
  | pi_sigma n f : Sigma n f -> Pi (S n) f
  | pi_univ n x f : Pi (S n) f -> Pi (S n) (funiv x f).

The following lemma suffices in essentially all cases, due to proof irrelevance:

Lemma Sigma_n_ind n : forall (P : arith_formula -> Prop),
  (forall f, Pi n f -> P f) ->
  (forall x f, Sigma (S n) f -> P f -> P (fexis x f)) ->
  forall f, Sigma (S n) f -> P f.
Proof.
  intros P Hpi Hexis f H.
  remember (S n) as m.
  induction H.
  - discriminate.
  - injection Heqm as Heqm. apply Hpi. rewrite <- Heqm. assumption.
  - apply Hexis. assumption. apply IHSigma; assumption.
Qed.

As far as I can tell, the remember is necessary. induction isn't smart enough to realize that the sigma_qf case is impossible, so we need to preserve enough information to prove that. Heqm : 0 = S n suffices, with a call to discriminate.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.