Inversion lemma for formulas

[Janis-Bai]

In the current version of the library, inversion on formulas is not working as expected. In some cases, for instance, congruence falls short of closing a goal s = t given the assumption q → s = q → t with s,t,q: form.

@yforster suggested to fix this by adding the following lemma to the library (formulation and proof are due to him):

Inductive aand (P Q R : Prop) :=
      cconj : P -> Q -> R -> aand P Q R.

Lemma form_inv {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ops : operators} {flag : falsity_flag} phi1 phi2 :
      phi1 = phi2 ->
      match phi1, phi2 with
      | falsity, falsity => True
      | atom _ P1 args1, atom _ P2 args2 => True
      | bin falsity_on o1 phi1' phi2', bin falsity_on o2 phi1'' phi2'' =>
            aand (o1 = o2) (phi1' = phi1'') (phi2' = phi2'')
      | bin falsity_off o1 phi1' phi2', bin falsity_off o2 phi1'' phi2'' =>
          aand (o1 = o2) (phi1' = phi1'') (phi2' = phi2'')
      | quant falsity_on o1 phi, quant falsity_on o2 phi' =>
            o1 = o2 /\ phi = phi'
      | quant falsity_off o1 phi, quant falsity_off o2 phi' =>
          o1 = o2 /\ phi = phi'
      | _, _ => False
      end.
Proof.
      intros H. destruct phi1; subst; eauto.
      all: destruct b; econstructor; eauto.
Qed.

[mrhaandi]

closing a goal s = t given the assumption q → s = q → t with s,t,q: form.

This known limitation of congruence should be fixed with rocq-prover/rocq#19700.

[DmxLarchey]

@Janis-Bai,

The type of first-order formulas is a dependent type. Inversion of identity equations over dependent types is not trivial. If the type of parameters is not discrete (ie with decidable equality, or unicity of identity proofs see below), then constructors may not even be provably injective.

In general, as @yforster suggests, it is a good idea to be able to write inversions of identity equations by hand. Typically, I suggest you try this one as a minimal exercise:

Section term_eq_inv. 

  Variables (I : Type) (f : I -> Type).
 
  Inductive term : Type :=
    | term_in i : f i -> term.

  Implicit Type t : term.

  Fact term_eq_inv i j a b : term_in i a = term_in j b -> exists e : i = j, eq_rect _ _ a _ e = b.
  Proof.
  Admitted.

Try a direct approach and see what happens with inversion for instance.

It is important to know that inversion, or more generally those proofs, are usually based on (possibly partial and dependent) projections and here I would suggest to use:

  Definition term_idx t :=
    match t with
    | term_in i _ => i
    end.

  Definition term_val t : f (term_idx t) :=
    match t with
    | term_in _ a => a
    end.

  Fact term_form_inv t j b : t = term_in j b -> exists e : term_idx t = j, eq_rect _ _ (term_val t) _ e = b.
  Proof.
  Admitted.

which gives the solution for term_eq_inv as just an instance of term_form_inv.
However, if you want to show:

Fact term_eq_inv' n a b : term_in n a = term_in n b -> a = b.

then you won't be able to get it unless the type index I has unicity of identity proofs, ie forall (i : I) (e : i = i), e = eq_refl.