Demo.v without tuples #271
Conversation
src/DemoWithReification.v
Outdated
| Local Ltac push := autorewrite with push_eval push_map distr_length | ||
| push_flat_map push_fold_right push_nth_default cancel_pair natsimplify. | ||
| Definition zeros n : list Z | ||
| := List.map (fun _ => 0) (seq 0 n). |
src/DemoWithReification.v
Outdated
| (weight_nz : forall i, weight i <> 0). | ||
|
|
||
| Definition to_associational (xs:list Z) : list (Z*Z) | ||
| := combine (map weight (List.seq 0 (List.length xs))) xs. |
There was a problem hiding this comment.
Add a nat argument for the length, require it to be equal to length xs as a precondition to the correctness proof. (I am not sure about this, but it seems like a direct translation from tuple code).
There was a problem hiding this comment.
Done. Turns out that precondition isn't needed to prove eval_to_associational. Should I insert it anyway? (And eval_add_to_nth could take a weaker hypothesis, namely i < min n (length xs) rather than i < length xs and n = length xs; which hypotheses should I use?
src/DemoWithReification.v
Outdated
| Section mulmod. | ||
| Context (m:Z) (m_nz:m <> 0) (s:Z) (s_nz:s <> 0) | ||
| (c:list (Z*Z)) (Hm:m = s - Associational.eval c). | ||
| Definition mulmod (a b:list Z) : list Z |
There was a problem hiding this comment.
Again, to blindly match the tuple code, I would add another argument that gets used as length a, length b, and max (length a) (length b).
_CoqProject
Outdated
| @@ -3,6 +3,7 @@ | |||
| Bedrock/Nomega.v | |||
| Bedrock/Word.v | |||
| src/Demo.v | |||
| src/DemoWithReification.v | |||
There was a problem hiding this comment.
Perhaps src/Experiments/SimplyTypedArithmetic ?
JasonGross
force-pushed
the
demo-no-tuples
branch
from
76634ef
to
666461a
Compare
|
Quoting #271 (comment) here so it's not collapsed:
@JasonGross said:
|
|
Looks good to me as-is, still. |
No description provided.