search

opencompl / lean-mlir

A minimal development of SSA theory
Other
88 stars 10 forks source link

llvm: BitVec.xor_neg_one will enable ring_nf to be more powerful #308

Open tobiasgrosser opened 5 months ago

tobiasgrosser commented 5 months ago

The pattern a ^^^ (-1#w) = (-1#w) - a arises several times in AliveStatements. Proofing it will in certain cases enable ring to close goals, but it also breaks certain extensionality proofs. We may want to use it carefully (meaning, only after the ext proof in alive_auto has been executed).

This should resolve four theorems.

bollu commented 5 months ago

Right. This is the type of thing that wants us to write an ad-hoc proof procedure, which tries multiple styles of proof, since there’s no good “normal form” for all cases we want to cover.

tobiasgrosser commented 5 months ago

This lemma appears in theorem bitvec_AddSub_1560 and might be a good next one for @eurquhart1.

emmau678 commented 1 month ago

Hi, I was just checking through and I see this was assigned to me and looks like it remains open (if so, I can try to complete it if it would still be useful?)