Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to automatically generate "good" names when decomposing existential hypothesis

Tags:

coq

I have an existential hypothesis, such as:

H : exists (a : A) (b : B) (c : C), P a b c

which I want to decompose to:

a : A
b : B
c : C
H0 : P a b c

The tactic decompose [ex] H; clear H does exactly this, except that the names of the variables become x, x0 and x1 rather than a, b, c. Is there any way to decompose this hypothesis, automatically generating "good" names (in the same way that intros would for a goal of forall (a : A) (b : B) (c : C), P a b c)?

like image 323
jchl Avatar asked Mar 14 '14 12:03

jchl


3 Answers

The following tactic (a simplified, tidied-up and corrected version of Vinz's solution) achieves the desired result.

Ltac decompose_ex H :=
  repeat match type of H with
           | ex (fun x => _) =>
             let x := fresh x in
             destruct H as [x H]
         end.
like image 199
jchl Avatar answered Nov 03 '22 14:11

jchl


Ok, I think I managed (with some help :D) to do what you wanted:

Parameter A B C : Type.
Parameter P : A -> B -> C -> Prop.
Parameter Q : Prop.

(* This will try to match an hypothesis named h with 'exists u: T, P' 
   and return the name of 'u' *)
Ltac extract_name h :=
  match goal with
    | [h : ?A |- _ ] => 
      match A with
        | @ex ?T ?P => match P with
                          | fun u => _ => u
                   end
   end
end.

(* 'smart' destruct using the name we just computed *)
Ltac one_destruct h :=
   let a := extract_name h in
   destruct h as [a h].

Goal (exists (a:A) (b:B) (c:C), P a b c) -> Q.
intros H.
repeat (one_destruct H).
(* the goal is now
1 subgoals
a : A
b : B
c : C
H : P a b c
______________________________________(1/1)
Q
*)

I am not a skilled Ltac user, so this might not be completely perfect. Use at your own risks :)

Best, V.

like image 26
Vinz Avatar answered Nov 03 '22 15:11

Vinz


It's possible to give the names manually.

Goal forall (t : Type) (p : t -> Prop) (q : Prop), (exists x : t, p x) -> q.
Proof. intros ? ? ? h1. elim h1. intros x h2. Abort.

Goal forall (t : Type) (p : t -> Prop) (q : Prop), (exists x : t, p x) -> q.
Proof. intros ? ? ? h1. inversion h1 as [x h2]. Abort.

Goal forall (t : Type) (p : t -> Prop) (q : Prop), (exists x : t, p x) -> q.
Proof. intros ? ? ? h1. destruct h1 as [x h2]. Abort.

Goal forall (t : Type) (p : t -> Prop) (q : Prop), (exists x : t, p x) -> q.
Proof. intros ? ? ? h1. induction h1 as [x h2]. Abort.

Goal forall (t : Type) (p : t -> Prop) (q : Prop), (exists x : t, p x) -> q.
Proof. intros ? ? ? [x h]. Abort.
like image 1
Rui Baptista Avatar answered Nov 03 '22 16:11

Rui Baptista