Update Curves/Weierstrass #1953
Conversation
| @@ -67,8 +67,8 @@ Module Jacobian. | |||
| | _ => progress destruct_head'_sum | |||
| | _ => progress destruct_head'_bool | |||
| | _ => progress destruct_head'_or | |||
| | H: context[@dec ?P ?pf] |- _ => destruct (@dec P pf) | |||
| | |- context[@dec ?P ?pf] => destruct (@dec P pf) | |||
| | H: context[@dec ?P ?pf] |- _ => destruct (@dec P pf) || destruct (@dec P pf) at 1 | |||
There was a problem hiding this comment.
@JasonGross this is because dependent occurrences and destructable occurranes of the same expression. Do you know a more systematic fix from the top of your head?
There was a problem hiding this comment.
Shouldn't it be "at 1 in H" or similar?
A more systematic fix: H: context C[@dec ?P ?pf] |- _ => destruct (@dec P pf) || (let p := fresh in pose (@dec P pf) as p; let C' := context C[p] in change C' in (type of H); destruct p)
Maybe too painful though
There was a problem hiding this comment.
is the idea that change works fine for changing some but not all occurrences?
There was a problem hiding this comment.
Yes, change + context will select only one occurrence at a time. This won't work if you need to simultaneously destruct in two or more occurrences though
| @@ -42,13 +42,53 @@ Module Jacobian. | |||
| | [ H : ?T, H' : ~?T |- _ ] => solve [ exfalso; apply H', H ] | |||
| end. | |||
|
|
|||
| Ltac lift_let := | |||
There was a problem hiding this comment.
@JasonGross do we have this somewhere already?
There was a problem hiding this comment.
https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/Tactics/MoveLetIn.v is similar but different.
I think this should get its own tactics file
No description provided.