The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

----- Mail original -----
> De: "Volker Stolz" 
> <stolz AT ifi.uio.no>
> À: 
> coq-club AT inria.fr
> Envoyé: Mardi 1 Décembre 2015 09:44:01
> Objet: Re: [Coq-Club] Problem proving "no number larger than n is in the 
> subset of numbers up to n"
> 
> Dear Laurent, dear Amin, thank you for your answers -- unfortunately
> they both seem to subvert the spirit of my original problem :-)
> 
> So here is my actual problem:
> 
> PF is a representation of propositional formulae bool
> True/False, props of some type, and negation on disjunction to build
> terms. That is, I have terms as a tree structure.
> 
> Section PF.
>   Variable A : Set.
> 
> Inductive pf : Type :=
> | bT : pf
> | bF : pf
> | p (a:A) : pf
> | neg (phi:pf) : pf
> | or (phi psi: pf) : pf.
> 
> Require Import Ensembles.
> Require Import Finite_sets.
> Require Import Finite_sets_facts.
> 
> Fixpoint sf phi : Ensemble pf :=
> match phi with
> | bT => Singleton pf bT
> | bF => Singleton _ bF
> | p x => Singleton _ (p x)
> | neg phi' => Add _ (sf phi') phi
> | or phi' psi' => Add _ (Union _ (sf phi') (sf psi')) phi
> end.
> 
> And here is my problematic property:
> 
> Hypothesis negNotInSelf: forall phi, ~In _ (sf phi) (neg phi).

A way to do this is to strengthen the property so that it can be proved
easily inductively. For instance:

1/ define pf_size as a Fixpoint measuring the size of a formula in pf. 

   pf_size : pf -> nat

2/ Then show that any subformula of phi (x s.t. In _ (sf phi) x)
   has a pf_size less than that of phi. This is an *easy* inductive proof
   on phi (use the omega tactic if you are lazy solving the inequations 
   between elements of nat).

   forall phi x, In _ (sf phi) x -> pf_size x <= pf_size phi

3/ Finally, show that the pf_size of neg phi is not less than that of phi
   which should hold for any reasonable definition of pf_size.

   forall phi, ~ (pf_size (neg phi) <= pf_size phi)

4/ conclude

Remark that you can replace pf_size by pf_height. There are certainly
numerous other options.

Best,

Dominique