Library Lambda.Tactics


Require
 Import
 Lambda.Utils.




Ltac
 destruct_one_pair
 :=

 match
 goal
 with


 | [H
 : (ex _
) |- _
] ⇒ destruct
 H


 | [H
 : (ex2 _
) |- _
] ⇒ destruct
 H


 | [H
 : (ex3 _
) |- _
] ⇒ destruct
 H


 | [H
 : (ex4 _
) |- _
] ⇒ destruct
 H


 | [H
 : (_
 ∧ _
) |- _
] ⇒ destruct
 H


end
.




Ltac
 destruct_exists
 := repeat
 (destruct_one_pair
) .




Ltac
 induction_with_subterm
 c
 H
 :=

  (set
(x
 := c
) ; assert
(y
:x = c
) by
 reflexivity
 ;

  rewrite
 <- y
 in
 H
 ; 

  induction
 H
 ; subst
).




Ltac
 induction_with_subterms
 c
 c'
 H
 :=

  let
 x
 := fresh
 "x" in


  let
 y
 := fresh
 "y" in


  let
 z
 := fresh
 "z" in


  let
 w
 := fresh
 "w" in


  (set
(x
 := c
) ; assert
(y
:x = c
) by
 reflexivity
 ;

  set
(z
 := c'
) ; assert
(w
:z = c'
) by
 reflexivity
 ;

  rewrite
 <- y
 in
 H
 ; rewrite
 <- w
 in
 H
 ; 

  induction
 H
 ; subst
).