How can I construct terms in first-order logic using Coq?

Link:: https://stackoverflow.com/q/64841759

Display all goals and responses

Question

I'm trying to define first-order logic in Coq and beginning at terms. Supposing that c1 and c2 are two constant symbols, variables are nat and f1 and f2 are two function symbols whose arities are 1 and 2 respectively, I wrote the following code.

Definition var := nat.

Inductive const : Type :=
| c1
| c2.

Inductive term : Type :=
| Con : const -> term
| Var : var -> term
| F1 : term -> term
| F2 : term -> term -> term.

Then, I got a desired induction.

Check term_ind.term_ind
     : forall P : term -> Prop,
       (forall c : const, P (Con c)) ->
       (forall v : var, P (Var v)) ->
       (forall t : term, P t -> P (F1 t)) ->
       (forall t : term,
        P t -> forall t0 : term, P t0 -> P (F2 t t0)) ->
       forall t : term, P t

Then I wanted to separate functions from the definition of term, so I rewrote the above.

(*Idea A*)
Inductive funct {X : Type} : Type :=
| f1 : X -> funct
| f2 : X -> X -> funct.

Inductive term : Type :=
| Con : const -> term
| Var : var -> term
| Fun : @funct term -> term.

Check term_ind.term_ind
     : forall P : term -> Prop,
       (forall c : const, P (Con c)) ->
       (forall v : var, P (Var v)) ->
       (forall f1 : funct, P (Fun f1)) ->
       forall t : term, P t
Check funct_ind term.funct_ind term
     : forall P : funct -> Prop,
       (forall x : term, P (f1 x)) ->
       (forall x x0 : term, P (f2 x x0)) ->
       forall f1 : funct, P f1

(*Idea B*)
Inductive term : Type :=
| Con : const -> term
| Var : var -> term
| Fun : funct -> term
with funct : Type :=
| f1 : term -> funct
| f2 : term -> term -> funct.

Check term_ind.term_ind
     : forall P : term -> Prop,
       (forall c : const, P (Con c)) ->
       (forall v : var, P (Var v)) ->
       (forall f1 : funct, P (Fun f1)) ->
       forall t : term, P t
Check funct_ind.funct_ind
     : forall P : funct -> Prop,
       (forall t : term, P (f1 t)) ->
       (forall t t0 : term, P (f2 t t0)) ->
       forall f1 : funct, P f1

However, both ways seem not to generate the desired induction because they don't have induction hypotheses.

How can I construct term with functions separated from the definition of term without loss of proper induction?

Thanks.

Answer

This is a common issue with Coq: the induction principles generated for mutually inductive types and for types with complex recursive occurrences are too weak. Fortunately, this can be fixed by defining the induction principles by hand. In your case, the simplest approach is to use the mutually inductive definition, since Coq can lend us a hand for proving the principle.

First, let ask Coq not to generate its weak default induction principle:

Unset Elimination Schemes.
Inductive term : Type :=
| Con : const -> term
| Var : var -> term
| Fun : funct -> term
with funct : Type :=
| f1 : term -> funct
| f2 : term -> term -> funct.
Set Elimination Schemes.

(This is not strictly necessary, but it helps keeping the global namespace clean.)

Now, let us use the Scheme command to generate a mutual induction principle for these types:

Scheme term_ind' := Induction for term Sort Prop
  with funct_ind' := Induction for funct Sort Prop.

term_ind'
     : forall (P : term -> Prop) (P0 : funct -> Prop),
       (forall c : const, P (Con c)) ->
       (forall v : var, P (Var v)) ->
       (forall f1 : funct, P0 f1 -> P (Fun f1)) ->
       (forall t : term, P t -> P0 (f1 t)) ->
       (forall t : term,
        P t -> forall t0 : term, P t0 -> P0 (f2 t t0)) ->
       forall t : term, P t

This principle is already powerful enough for us to prove properties of term, but it is a bit awkward to use, since it requires us to specify a property that we want to prove about the funct type as well (the P0 predicate). We can simplify it a bit to avoid mentioning this auxiliary predicate: all we need to know is that the terms inside the function calls satisfy the predicate that we want to prove.

Definition lift_pred (P : term -> Prop) (f : funct) : Prop :=
  match f with
  | f1 t => P t
  | f2 t1 t2 => P t1 /\ P t2
  end.

Lemma term_ind (P : term -> Prop) :
  (forall c, P (Con c)) ->
  (forall v, P (Var v)) ->
  (forall f, lift_pred P f -> P (Fun f)) ->
  forall t, P t.P: term -> Prop
(forall c : const, P (Con c)) ->
(forall v : var, P (Var v)) ->
(forall f : funct, lift_pred P f -> P (Fun f)) ->
forall t : term, P t
Proof.P: term -> Prop
(forall c : const, P (Con c)) ->
(forall v : var, P (Var v)) ->
(forall f : funct, lift_pred P f -> P (Fun f)) ->
forall t : term, P t
  intros HCon HVar HFun.P: term -> Prop
HCon: forall c : const, P (Con c)
HVar: forall v : var, P (Var v)
HFun: forall f : funct, lift_pred P f -> P (Fun f)
forall t : term, P t
  apply (term_ind' P (lift_pred P)); trivial.P: term -> Prop
HCon: forall c : const, P (Con c)
HVar: forall v : var, P (Var v)
HFun: forall f : funct, lift_pred P f -> P (Fun f)
forall t : term,
P t -> forall t0 : term, P t0 -> lift_pred P (f2 t t0)
  now intros t1 IH1 t2 IH2; split.
Qed.

If you prefer, you can also rewrite this to look more like the original induction principle:

Reset term_ind.
Lemma term_ind (P : term -> Prop) :
  (forall c, P (Con c)) ->
  (forall v, P (Var v)) ->
  (forall t, P t -> P (Fun (f1 t))) ->
  (forall t1, P t1 -> forall t2, P t2 -> P (Fun (f2 t1 t2))) ->
  forall t, P t.P: term -> Prop
(forall c : const, P (Con c)) ->
(forall v : var, P (Var v)) ->
(forall t : term, P t -> P (Fun (f1 t))) ->
(forall t1 : term,
 P t1 -> forall t2 : term, P t2 -> P (Fun (f2 t1 t2))) ->
forall t : term, P t
Proof.P: term -> Prop
(forall c : const, P (Con c)) ->
(forall v : var, P (Var v)) ->
(forall t : term, P t -> P (Fun (f1 t))) ->
(forall t1 : term,
 P t1 -> forall t2 : term, P t2 -> P (Fun (f2 t1 t2))) ->
forall t : term, P t
  intros HCon HVar HFun_f1 HFun_f2.P: term -> Prop
HCon: forall c : const, P (Con c)
HVar: forall v : var, P (Var v)
HFun_f1: forall t : term, P t -> P (Fun (f1 t))
HFun_f2: forall t1 : term,
P t1 ->
forall t2 : term, P t2 -> P (Fun (f2 t1 t2))
forall t : term, P t
  apply (term_ind' P (lift_pred P)); trivial.P: term -> Prop
HCon: forall c : const, P (Con c)
HVar: forall v : var, P (Var v)
HFun_f1: forall t : term, P t -> P (Fun (f1 t))
HFun_f2: forall t1 : term,
P t1 ->
forall t2 : term, P t2 -> P (Fun (f2 t1 t2))
forall f : funct, lift_pred P f -> P (Fun f)
P: term -> Prop
HCon: forall c : const, P (Con c)
HVar: forall v : var, P (Var v)
HFun_f1: forall t : term, P t -> P (Fun (f1 t))
HFun_f2: forall t1 : term,
P t1 ->
forall t2 : term, P t2 -> P (Fun (f2 t1 t2))
forall t : term,
P t -> forall t0 : term, P t0 -> lift_pred P (f2 t t0)
  -P: term -> Prop
HCon: forall c : const, P (Con c)
HVar: forall v : var, P (Var v)
HFun_f1: forall t : term, P t -> P (Fun (f1 t))
HFun_f2: forall t1 : term,
P t1 ->
forall t2 : term, P t2 -> P (Fun (f2 t1 t2))
forall f : funct, lift_pred P f -> P (Fun f) now intros [t | t1 t2]; simpl; intuition.
  -P: term -> Prop
HCon: forall c : const, P (Con c)
HVar: forall v : var, P (Var v)
HFun_f1: forall t : term, P t -> P (Fun (f1 t))
HFun_f2: forall t1 : term,
P t1 ->
forall t2 : term, P t2 -> P (Fun (f2 t1 t2))
forall t : term,
P t -> forall t0 : term, P t0 -> lift_pred P (f2 t t0) now simpl; intuition.
Qed.

Edit

To get an induction principle for your other approach, you have to write a proof term by hand:

Definition var := nat.

Inductive const : Type :=
| c1
| c2.

Inductive funct (X : Type) : Type :=
| f1 : X -> funct X
| f2 : X -> X -> funct X.
Arguments f1 {X} _.
Arguments f2 {X} _ _.

Unset Elimination Schemes.
Inductive term : Type :=
| Con : const -> term
| Var : var -> term
| Fun : funct term -> term.
Set Elimination Schemes.

Definition term_ind (P : term -> Type)
           (HCon : forall c, P (Con c))
           (HVar : forall v, P (Var v))
           (HF1  : forall t, P t -> P (Fun (f1 t)))
           (HF2  : forall t1, P t1 -> forall t2, P t2 -> P (Fun (f2 t1 t2))) :
  forall t, P t :=
  fix loop (t : term) : P t :=
    match t with
    | Con c => HCon c
    | Var v => HVar v
    | Fun (f1 t) => HF1 t (loop t)
    | Fun (f2 t1 t2) => HF2 t1 (loop t1) t2 (loop t2)
    end.