2
$\begingroup$

I've been working on formalizing a Hilbert deductive system within Coq. I have the following definition for a term in first-order logic:

Inductive term : Type :=
  | tvar : variable -> term
  | tfunc {n} : function n -> Vector.t term n -> term.

Definition args := Vector.t term.

Note that function : nat -> Type is a parameter of the section.

I find myself having to write the following very specific induction scheme for the type, in order to prove certain theorems (specifically, to prove theorems about substitution of a variable with another term):

Lemma term_dbl : forall (P : term -> term -> Prop),
  (forall x r, P (tvar x) r) ->
  (forall n (f : function n) a x, P (tfunc f a) (tvar x)) ->
  (forall {n} (f g : function n) a b, Vector.Forall2 P a b -> P (tfunc f a) (tfunc g b)) ->
  forall t t', P t t'.

By taking inspiration from the mutual induction scheme I already wrote, and the standard library member Vector.rect2, I came up with the following almost-solution:

Fixpoint term_dbl (P : term -> term -> Prop)
  (Hbase : forall x r, P (tvar x) r)
  (Hcontra : forall {n} (f : function n) a x, P (tfunc f a) (tvar x))
  (Hstep : forall {n} (f g : function n) a b, Vector.Forall2 P a b -> P (tfunc f a) (tfunc g b))
  t t' {struct t} : P t t' :=
  match t with
  | tvar x => Hbase x t'
  | tfunc f a => match t' with
    | tvar x => Hcontra f a x
    | tfunc g b => let fix term_dbl_fix {n} (a' b' : args n) : Vector.Forall2 P a' b' :=
      match a' with
      | Vector.nil _ => Vector.case0 _ Vector.Forall2_nil (b' : args 0)
      | Vector.cons _ ha n' ta => Vector.caseS' b' (fun b'' => Vector.Forall2 P (Vector.cons _ ha _ ta) b'')
        (fun hb tb => Vector.Forall2_cons ha hb ta tb (term_dbl P Hbase Hcontra Hstep ha hb) (term_dbl_fix ta tb))
      end
      in Hstep f g a b (term_dbl_fix a b)
    end
  end.

As far as I can tell, the only problem with the definition is one of unification. The error message is:

The term "b'" has type "args n1" while it is expected to have type "args 0".

in the term b' : args 0. (I added the explicit type annotation for clarity; error appears without it). I assume there will be problems with the second branch as well, if the first did not error.

I would expect the pattern-match on a' to prove that n = 0, but this is not what happens. Is there a way to modify this function to be accepted by Coq? And/or, is there an alternative way to prove this induction scheme?

EDIT:

I've added a branch for functions of differing arities.

Fixpoint term_dbl (P : term -> term -> Prop)
  (Hbase : forall x r, P (tvar x) r)
  (Hcontra : forall {n} (f : function n) a x, P (tfunc f a) (tvar x))
  (Hcontra' : forall m n (f : function m) (g : function n) a b, m <> n -> P (tfunc f a) (tfunc g b))
  (Hstep : forall {n} (f g : function n) a b, Vector.Forall2 P a b -> P (tfunc f a) (tfunc g b))
  t t' {struct t} : P t t' :=
  match t with
  | tvar x => Hbase x t'
  | @tfunc m f a => match t' with
    | tvar x => Hcontra f a x
    | @tfunc n g b => match Nat.eq_dec m n with
      | left eq_refl => let fix term_dbl_fix {n'} (a' b' : args n') : Vector.Forall2 P a' b' :=
        match a' with
        | Vector.nil _ => Vector.case0 _ Vector.Forall2_nil b'
        | Vector.cons _ ha _ ta => Vector.caseS' b' (fun b'' => Vector.Forall2 P (Vector.cons _ ha _ ta) b'')
          (fun hb tb => Vector.Forall2_cons ha hb ta tb (term_dbl P Hbase Hcontra Hstep ha hb) (term_dbl_fix ta tb))
        end
        in Hstep f g a b (term_dbl_fix a b)
      | right contra => Hcontra' contra
      end
    end
  end.

However, the specific error has not changed: cannot unify "n'" and "0".

EDIT 2:

Finally got it working:

Lemma term_dbl : forall (P : term -> term -> Prop),
  (forall x r, P (tvar x) r) ->
  (forall {n} (f : function n) a x, P (tfunc f a) (tvar x)) ->
  (forall {m n} (f : function m) (g : function n) a b, m <> n -> P (tfunc f a) (tfunc g b)) ->
  (forall {n} (f g : function n) a b, Vector.Forall2 P a b -> P (tfunc f a) (tfunc g b)) ->
  forall t t', P t t'.
Proof.
  intros P Hbase Hcontra Hcontra' Hstep.
  refine (fix term_dbl_fix t t' {struct t} := match t with
    | tvar x => _
    | @tfunc m f a => _
  end).
  - apply Hbase.
  - destruct t' as [y|n g].
    + apply Hcontra.
    + specialize (Nat.eq_dec m n) as E.
      destruct E.
      * destruct e.
        apply Hstep.
        clear f. clear g. clear t.
        induction a.
        --  apply (Vector.case0 _ (Vector.Forall2_nil P) t0).
        --  apply (Vector.caseS' t0 _ (fun hb tb => Vector.Forall2_cons P h hb a tb (term_dbl_fix h hb) (IHa tb))).
      * apply Hcontra'. assumption.
Qed.
Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

Coq complains with reason: there is a priori no reason why the number of arguments of the two functions you are comparing have to be the same. And, indeed, you lemma is false!

Require Import Vector.

Import VectorNotations.

Section Test.
  Variable (variable : Type) (function : nat -> Type).

Unset Elimination Schemes.

Inductive term : Type :=
  | tvar : variable -> term
  | tfunc {n} : function n -> Vector.t term n -> term.

Set Elimination Schemes.

Definition args := Vector.t term.

Variable (f : function 0) (g : function 1) (x : variable).

Definition term1 := tfunc f [].
Definition term2 := tfunc g [tvar x].

Definition P (t t' : term) : Prop :=
  match t, t' with
  | @tfunc 0 _ _, @tfunc 1 _ _ => False
  | _, _ => True
  end.

Lemma Pvar : forall x r, P (tvar x) r.
Proof.
  easy.
Qed.

Lemma Pfunvar : forall n (f : function n) a x, P (tfunc f a) (tvar x).
Proof.
  now intros [].
Qed.

Lemma Pfunfun : forall n (f g : function n) a b, Vector.Forall2 P a b -> P (tfunc f a) (tfunc g b).
Proof.
  now intros [].
Qed.

Lemma notP : exists t t', ~ (P t t').
Proof.
  now exists term1, term2.
Qed.

You should generalize the last case of your custom induction to somehow handle that case where the two functions have different arities. In case you need it, at least the unary induction principle is easy enough to prove:

Lemma term_ind : forall (P : term -> Prop),
  (forall x, P (tvar x)) ->
  (forall n (f : function n) (a : args n), Vector.Forall P a -> P (tfunc f a)) ->
  forall t, P t.
Proof.
  intros P Hvar Hfun.
  refine (
  fix ind (t : term) {struct t} : P t := match t with
  | tvar x => _
  | tfunc f a => _
  end).
  - apply Hvar.
  - apply Hfun.
    refine ((fix ind_vec (m : nat) (v : Vector.t term m) {struct v} : Forall P v :=
      match v with
      | [] => _
      | hd :: tl => _
    end) n a).
    + constructor.
    + constructor.
      * apply ind.
      * apply ind_vec.
Qed.
Improve this answer
$\endgroup$
2
  • $\begingroup$ Thank you. refine is a lifesaver! $\endgroup$
    – Circuit Craft
    Jun 9 at 21:36
  • $\begingroup$ If you try to prove fancy induction principles using proof mode and refine, a nice helper is Guarded., which tells you whether the term you built up to this point passes the guardedness checker. This lets you check as you go that the proof you construct will end up being accepted at Qed, since proof mode tactics never runs the guard checker (which is a global check of the whole proof term). $\endgroup$
    – Meven Lennon-Bertrand
    Jun 11 at 8:15

Your Answer

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

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