The Coq mailing list

[Vincent Demange <vincent.demange AT ensiie.fr>]

Hi MathProver,

Here I come with another solution (source file joined):

the idea is to prove
(P_0 -> ... -> P_n -> B_0 /\ ... B_m) ->
   /\_i (P_0 -> ... -> P_n -> B_i)

then by applying it to an hypothesis of the form
(P_0 -> ... -> P_n -> B_0 /\ ... /\ B_m)

we can generate all the hypotheses you want
(P_0 -> ... -> P_n -> B_i)


Since P_0 -> ... -> P_n -> B_0 is expressed by induction on the list
[P_0; ...; P_n], and And also, we need to use tactics to build those
lists.


The resulting proof term is small and beautiful !


Cheers,
Vincent.

Le lundi 17 juin 2013 à 02:16 -0700, Math Prover a écrit :
> Hi,
> 
> 
>   I want to destruct a "scoped and". See attached tac.v
> 
> 
>   My existing implementation is somewhat ugly -- for each length, I
> need to create (a) two lemmas and (b) an extra line in the tactic.
> 
> 
>   I was wondering if there was a simpler way to do this in "one shot"

(* And [Q_0; ...; Q_n] := Q_0 /\ ... /\ Q_n *)
Fixpoint And (l: list Prop) : Prop :=
  match l with
  | nil => True
  | cons p nil => p
  | cons p l' => and p (And l')
  end.

(* Imp [P_0; ...; P_n] B := P_0 -> ... -> P_n -> B *)
Fixpoint Imp (l: list Prop) (B:Prop) : Prop :=
  match l with
  | nil => B
  | cons p l' => p -> (Imp l' B)
  end.

(* Extended modus Ponens to Imp:
  (P_0 -> ... -> P_n -> B) -> (B -> C) -> (P_0 -> ... -> P_n -> C)
*)
Lemma ImpMP lP B (C: Prop):
  (Imp lP B) -> (B -> C) -> Imp lP C.
Proof.
induction lP; simpl.
  intros x f; exact (f x).
  intros f g x; apply IHlP.
    exact (f x).
    exact g.
Qed.


Require Import List.

(* Induction principle associated to the definition of And *)
Definition list_rect2 (A:Type) (P:list A -> Type)
  (Hnil:P nil) (Hone: forall a, P (cons a nil))
  (Hrec: forall (a b:A) (l:list A), P l -> P (cons a (cons b l)))
  : forall (l: list A), P l :=
  fix F (l : list A) : P l :=
  match l as r return P r with
  | nil => Hnil
  | cons p nil => Hone p
  | cons p (cons q l') =>  Hrec p q l' (F l')
  end.

(* Now the main result:
  (P_0 -> ... -> P_n -> B_0 /\ ... B_m) ->
   /\ (P_0 -> ... -> P_n -> B_i)
 *)
Theorem ImpAnd_AndImp lP lB:
  Imp lP (And lB) -> And ( List.map (fun B => Imp lP B) lB).
Proof.
revert lP; induction lB using list_rect2; intro lP; simpl.
  intros _; constructor.
  intros x; exact x.
  revert IHlB lP; case lB; clear lB.
    simpl.
    intros _ lP H; split; apply (ImpMP _ _ _ H); intros (x,y); assumption.
    intros B lB IHlB lP H; split.
      apply (ImpMP _ _ _ H); intros (x,_); exact x.
      red; split.
        apply (ImpMP _ _ _ H); intros (_,(x,_)); exact x.
        apply IHlB.
        apply (ImpMP _ _ _ H); intros (_,(_,x)); exact x.
Qed.


(* Construct the list lB from a formula F *)
Ltac constr_lB F :=
  match F with
  | and ?B ?C =>
    let lC := constr_lB C in
    constr:(cons B lC)
  | ?C =>
    constr:(cons C nil)
  end.

(* Construct the list lP from a formula F *)
Ltac constr_lP F :=
  match F with
  | ?P -> ?Q =>
    let lQ := constr_lP Q in
    constr:(cons P lQ)
  | _ => constr:(@nil Prop)
  end.

(* Get the 'tail' of the formule F, i.e.
  tail_lP (P_0 -> ... -> P_n -> B) := B
*)
Ltac tail_lP F :=
  match F with
  | _ -> ?Q =>
    tail_lP Q
  | _ => F
  end.

(* Get the type of a given hypothesis *)
Ltac get_type H :=
  match goal with
  | [H:?T |- _ ] => T
  end.

(* Destruct and hypothesis H : Q_0 /\ ... /\ Q_m
  into the hypotheses H_i: Q_i
*)
Ltac repeat_destruct H :=
  match goal with
  | [H:and ?A ?B |- _ ] => 
    let hyp := fresh H in
    destruct H as (H,hyp);
    repeat_destruct hyp
  | _ => idtac
  end.

(* Destruct an hypothesis H: P_0 -> ... -> P_n -> B_0 /\ ... B_m
  into the hypotheses   H_i: P_0 -> ... -> P_n -> B_i
*)
Ltac break_and H :=
  let T := get_type H in
  let lP := constr_lP T in
  let tl := tail_lP T in
  let lB := constr_lB tl in
  let hyp := fresh "_"H in
    assert (hyp := ImpAnd_AndImp lP lB);
    simpl Imp in hyp; simpl And in hyp;
  let hyp' := fresh H in
    assert (hyp' := hyp H); clear hyp;
    repeat_destruct hyp'.


Lemma want_to_prove:
  forall (p1 p2 p3 q1 q2 q3 q4 q5:  Prop),
    (p1 -> p2 -> p3 -> (q1 /\ q2 /\ q3 /\ q4)) -> q5.
  intros.
  break_and H.
  (* Show Proof. *) (* small proof term *)