Paco uses the JMeq_eq axiom (JMeq x y -> x = y) in the pcofix tactic (in pacotac_internal.v). The gist of what it's doing is to reshape the goal into a form where the pacoN_acc lemma can be applied, and JMeq_eq is used somewhere in this transformation. I'm wondering whether this can be simplified, in a way that doesn't use JMeq_eq.
As I understand it, pcofix needs to do the following.
Initial goal:
===================
forall x y z, hyps -> paco2 gf bot2 (f x y) (g z)
"uncurry" the goal
===================
forall a b, (exists x y z, hyps /\ existT _ a b = existT _ (f x y) (g z)) -> paco2 gf bot2 a b
apply paco2_acc
r : forall a b, Prop
COFIX : forall a b, (exists x y z, hyps /\ existT _ a b = existT _ (f x y) (g z)) -> r a b
===================
forall a b, (exists x y z, hyps /\ existT _ a b = existT _ (f x y) (g z)) -> paco2 gf r a b
"curry" the goal
r : forall a b, Prop
COFIX : forall a b, (exists x y z, hyps /\ existT _ a b = existT _ (f x y) (g z)) -> r a b
===================
forall x y z, hyps -> paco2 gf r (f x y) (g z)
"curry" the hypothesis
r : forall a b, Prop
COFIX : forall x y z, hyps -> r (f x y) (g z)
===================
forall x y z, hyps -> paco2 gf r (f x y) (g z)
JMeq_eq may seem necessary to rewrite between R a b and R (f x y) (g z) given only existT _ a b = existT _ (f x y) (g z), but this can actually be done without axioms by simply converting R a b to R (projT1 (existT _ a b)) (projT2 (existT _ a b)), and then rewriting with the above.
I think all of these steps are relatively straightforward (in fact I've already done most of the work once
|
Ltac uncurry_hyp OBG := |
|
let t := fresh "t" in |
|
unshelve refine (let t : telescope := _ in _); |
|
[ repeat lazymatch type of OBG with |
|
| forall x : ?A, _ => |
|
apply (@tscp A); |
|
let x := fresh x in |
|
intros x; |
|
specialize (OBG x) |
|
| ?T => apply (tscp0 T) |
|
end |
|
| cut (forall x, teleprop t x); subst t; cbv [telesig teleprop]; |
|
[ clear OBG; intros OBG |
|
| intros x; |
|
let rec go t := assumption + specialize (OBG (paco_projT1 t)); go (paco_projT2 t) in |
|
go x |
|
] |
|
]. |
|
|
|
Ltac curry_hyp OBG := |
|
let t := fresh "t" in |
|
unshelve refine (let t : telescope := _ in _); |
|
[ repeat lazymatch type of OBG with |
|
| forall _ : paco_sigT (fun x : ?A => _), _ => |
|
apply (@tscp A); |
|
let x := fresh x in |
|
intros x; |
|
let OBG' := fresh OBG in |
|
rename OBG into OBG'; |
|
pose proof (paco_sigT_curry_ OBG' x) as OBG; clear OBG'; |
|
cbn [paco_projT1 paco_projT2] in OBG |
|
| True -> ?T => apply (tscp0 T) |
|
end |
|
| cbv zeta beta in t; |
|
cut (teleforall t); subst t; cbv [ teleforall ]; |
|
[ clear OBG; intros OBG |
|
| repeat lazymatch goal with |
|
| [ |- forall x : _, _ ] => |
|
let x := fresh x in |
|
intros x; |
|
let OBG' := fresh OBG in |
|
rename OBG into OBG'; |
|
pose proof (paco_sigT_curry_ OBG' x) as OBG; clear OBG'; |
|
cbn [paco_projT1 paco_projT2] in OBG |
|
end; |
|
exact (OBG I) |
|
] |
|
]. |
|
|
|
Section TEST. |
|
|
|
Context (hyp : forall (x y z : nat), Prop). |
|
Context (goal : forall (u v w : bool), Prop). |
|
|
|
Lemma TEST |
|
(H : forall x y z : nat, x < z -> hyp x y z) : |
|
forall u v w, u = true -> goal u v w. |
|
Proof. |
|
uncurry_hyp H. |
|
curry_hyp H. |
|
uncurry_goal. |
|
curry_goal. |
|
Abort. |
|
|
|
End TEST. |
, it is currently commented out because of definitions that no longer exist, but I can restore and polish the whole thing), that's why I'm a bit surprised at the complexity of the existing definition of the
pcofix tactic. Am I missing some nuance about what
pcofix needs to do?
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent