Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.)


Chronological Thread 
  • From: Cao Qinxiang <caoqinxiang AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.)
  • Date: Mon, 16 Apr 2018 00:27:28 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=caoqinxiang AT gmail.com; spf=Pass smtp.mailfrom=caoqinxiang AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f51.google.com
  • Ironport-phdr: 9a23:6oy1rBw+bOR/uXPXCy+O+j09IxM/srCxBDY+r6Qd1OgQIJqq85mqBkHD//Il1AaPAd2Araocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HdbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHohikJNCM3/n/LhcFrlq1XvAisqgZjz4LIYoyYMud1cKPHfdMdQGpMRthcWDZGAoihdIUPDuwBPOlZr4bnoVsOoga1CA6wC+z1zT9In3723as10uQgCw7G2gMgEskBsHTRttr1NaMSXfqpw6nPyDXOdvVb0irz5ojPdxAuu/CMXbRofMrQz0kvDQLFgU+KpYzrJTOY0PkGvWuD7+d4S+6jl2oqpxtyrzWv3MsglJTFi4IPxl3E6Cl0xps+K8eiR05he9GkFYNdtyGEOItyRcMvW2Rotzw7yr0CoJK7eCYKxIg+yx7Ra/GLbpKE4h3kVOaWLjd4gGxqdKijiBa19Eis0uz8Vs+q31ZWtidJjMXAu3QX2xHQ6sWLUOVx8lqh1DqV1w3f9/lIIUUumqraL54hzKQwlp0WsUnbAiD5gkL2jLaXdkUi9emo6v7oYrPpppKHOI90jxvxMqUqmsClHes4NQ0OU3CB+eugzL3j4VH5QLJSg/IqlanZqYnWKtgfpq6kGABYyZ0j6ha6Dze+ytsUh3gHLFRfeBKGlYflIV/OIOqrRcu41l+riXJgw+3MFrznGJTEaHbZw5n7erMowEdbgDMyy8Be7pRbQuUKKfXqW0nhtdXeATc2NgW1x6DsD9ArhdBWYn6GHqLMaPCailSP/O96e7DdNr9Qgy70Lr0e39CriHY4nVEHeqzwhMkYbXm5GrJtJEDLOCOw0OdEKn8Du08FdMKvkEeLCGcBaHO7XqZ67TY+Wtr/UNXzA7u1ibnE5x+VW51bYmccVwKJGHbsMoGKA7ICNXvULchmnTgJE7OmTt152A==
Hello,

Do you have any idea why the following tactics fail?

Best,
Qinxiang

Ltac foo_tac tac :=
try tac.

Ltac TA1 :=
match goal with
| |- _ _  => idtac
end.

Ltac TA2 :=
match goal with
| |- _ _  => idtac
| |- _ => idtac
end.


Goal True.
foo_tac TA2. (* This succeed. *)
foo_tac TA1. (* WHY fail? *)
foo_tac destruct_one_ex.  (* This succeed. *)

Ltac destruct_one_ex := (* copied from https://coq.inria.fr/library/Coq.Program.Tactics.html *)
  let tac H := let ph := fresh "H" in (destruct H as [H ph]) in
  let tac2 H := let ph := fresh "H" in let ph' := fresh "H" in 
    (destruct H as [H ph ph']) 
  in
  let tacT H := let ph := fresh "X" in (destruct H as [H ph]) in
  let tacT2 H := let ph := fresh "X" in let ph' := fresh "X" in 
    (destruct H as [H ph ph']) 
  in
    match goal with
      | [H : (ex _) |- _] => tac H
      | [H : (sig ?P) |- _ ] => tac H
      | [H : (sigT ?P) |- _ ] => tacT H
      | [H : (ex2 _ _) |- _] => tac2 H
      | [H : (sig2 ?P _) |- _ ] => tac2 H
      | [H : (sigT2 ?P _) |- _ ] => tacT2 H
    end.

foo_tac destruct_one_ex. (* WHY fail? *)

Archive powered by MHonArc 2.6.18.

Top of Page