Can't `refl` simple equation

Stream: new members

[Marcus Rossel]

I have this goal state:

p p' : ports
h : list.length p' < list.length p
⊢ list.length p' + (list.length p - list.length p') = list.length p

... and neither refl, finish, library_search, hint, nor suggest close the goal or suggest a solution. Is this normal?

Those "ports"-things are defined as:

def ports := list (option value)

[Damiano Testa]

Are those natural numbers? There is something along the lines of add_sub_cancel in nat, I think.

[Patrick Massot]

Does omega work?

[Marcus Rossel]

Patrick Massot said:

Does omega work?

What's omega?

[Kevin Buzzard]

If you've imported tactic, just try it

[Patrick Massot]

The answer to this question is: no it's not normal, there should be a come_on_lean tactic closing this goal and thousands of similarly silly goals. But it's unfortunately expected.

[Kevin Buzzard]

Try writing "and now it's obvious" in French and see if it closes the goal. Apparently this sometimes works now!

[Marcus Rossel]

omega worked! Thanks guys

[Damiano Testa]

This also works:

lemma simple {a b c : ℕ} {h : a < b} : a + (b - a) = b :=
begin
  rw [← nat.add_sub_assoc (le_of_lt h), nat.add_sub_cancel_left],
end

[Kevin Buzzard]

(and it's probably faster)

[Patrick Massot]

The funny thing is the fact you have a strict inequality is probably making it more difficult for automation.

[Damiano Testa]

The omega way:

exact (id
   ((propext imp_iff_not_or).trans
      ((λ (a a_1 : Prop) (e_1 : a = a_1) (b b_1 : Prop) (e_2 : b = b_1), congr (congr_arg or e_1) e_2) (¬a + 1 ≤ b)
         (b + 1 ≤ a + 1)
         ((propext not_le).trans (propext nat.lt_iff_add_one_le))
         (a + (b - a) = b)
         (a + (b - a) = b)
         (eq.refl (a + (b - a) = b))))).mpr
  (omega.nat.univ_close_of_unsat_neg_elim_not 2
     ((omega.nat.preform.le ((omega.nat.preterm.var 1 1).add (omega.nat.preterm.cst 1))
         ((omega.nat.preterm.var 1 0).add (omega.nat.preterm.cst 1))).or
        (omega.nat.preform.eq
           ((omega.nat.preterm.var 1 0).add ((omega.nat.preterm.var 1 1).sub (omega.nat.preterm.var 1 0)))
           (omega.nat.preterm.var 1 1)))
     (omega.nat.unsat_of_unsat_sub_elim (omega.nat.preterm.var 1 1) (omega.nat.preterm.var 1 0)
        ((omega.nat.preform.le
            (((omega.nat.preterm.var 1 0).add (omega.nat.preterm.cst 1)).add (omega.nat.preterm.cst 1))
            ((omega.nat.preterm.var 1 1).add (omega.nat.preterm.cst 1))).and
           ((omega.nat.preform.le
               (((omega.nat.preterm.var 1 0).add ((omega.nat.preterm.var 1 1).sub (omega.nat.preterm.var 1 0))).add
                  (omega.nat.preterm.cst 1))
               (omega.nat.preterm.var 1 1)).or
              (omega.nat.preform.le ((omega.nat.preterm.var 1 1).add (omega.nat.preterm.cst 1))
                 ((omega.nat.preterm.var 1 0).add ((omega.nat.preterm.var 1 1).sub (omega.nat.preterm.var 1 0))))))
        (omega.nat.unsat_of_unsat_dnf
           (((omega.nat.preform.le
                (((omega.nat.preterm.var 1 0).add (omega.nat.preterm.cst 1)).add (omega.nat.preterm.cst 1))
                ((omega.nat.preterm.var 1 1).add (omega.nat.preterm.cst 1))).and
               ((omega.nat.preform.le
                   (((omega.nat.preterm.var 1 0).add (omega.nat.preterm.var 1 2)).add (omega.nat.preterm.cst 1))
                   (omega.nat.preterm.var 1 1)).or
                  (omega.nat.preform.le ((omega.nat.preterm.var 1 1).add (omega.nat.preterm.cst 1))
                     ((omega.nat.preterm.var 1 0).add (omega.nat.preterm.var 1 2))))).and
              ((omega.nat.preform.eq (omega.nat.preterm.var 1 1)
                  ((omega.nat.preterm.var 1 0).add (omega.nat.preterm.var 1 2))).or
                 ((omega.nat.preform.le (omega.nat.preterm.var 1 1) (omega.nat.preterm.var 1 0)).and
                    (omega.nat.preform.eq (omega.nat.preterm.var 1 2) (omega.nat.preterm.cst 0)))))
           ⟨⟨trivial, ⟨trivial, trivial⟩⟩, ⟨trivial, ⟨trivial, trivial⟩⟩⟩
           ⟨⟨⟨⟨⟨trivial, trivial⟩, trivial⟩, ⟨trivial, trivial⟩⟩,
             ⟨⟨⟨⟨trivial, trivial⟩, trivial⟩, trivial⟩,
              ⟨⟨trivial, trivial⟩, ⟨trivial, trivial⟩⟩⟩⟩,
            ⟨⟨trivial, ⟨trivial, trivial⟩⟩, ⟨⟨trivial, trivial⟩, ⟨trivial, trivial⟩⟩⟩⟩
           (omega.clauses.unsat_cons
              ([(int.of_nat 0, [int.of_nat 1, -[1+ 0], int.of_nat 1])],
               [(int.of_nat 0, [int.of_nat 1]), (int.of_nat 0, [int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                  [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0], [-[1+ 0], int.of_nat 1]), (-[1+ 0],
                  [-[1+ 0], int.of_nat 1, -[1+ 0]])])
              [([(int.of_nat 0, [int.of_nat 0, int.of_nat 0, -[1+ 0]])],
                 [(int.of_nat 0, [int.of_nat 1]), (int.of_nat 0, [int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                    [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0], [-[1+ 0], int.of_nat 1]), (-[1+ 0],
                    [-[1+ 0], int.of_nat 1, -[1+ 0]]), (int.of_nat 0, [int.of_nat 1, -[1+ 0]])]), ([(int.of_nat 0,
                    [int.of_nat 1, -[1+ 0], int.of_nat 1])],
                 [(int.of_nat 0, [int.of_nat 1]), (int.of_nat 0, [int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                    [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0], [-[1+ 0], int.of_nat 1]), (-[1+ 0],
                    [int.of_nat 1, -[1+ 0], int.of_nat 1])]), ([(int.of_nat 0, [int.of_nat 0, int.of_nat 0, -[1+ 0]])],
                 [(int.of_nat 0, [int.of_nat 1]), (int.of_nat 0, [int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                    [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0], [-[1+ 0], int.of_nat 1]), (-[1+ 0],
                    [int.of_nat 1, -[1+ 0], int.of_nat 1]), (int.of_nat 0, [int.of_nat 1, -[1+ 0]])])]
              (omega.unsat_of_unsat_eq_elim [omega.ee.factor (int.of_nat 1), omega.ee.cancel 0]
                 ([(int.of_nat 0, [int.of_nat 1, -[1+ 0], int.of_nat 1])],
                  [(int.of_nat 0, [int.of_nat 1]), (int.of_nat 0, [int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                     [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0], [-[1+ 0], int.of_nat 1]), (-[1+ 0],
                     [-[1+ 0], int.of_nat 1, -[1+ 0]])])
                 (omega.unsat_of_unsat_lin_comb [0, 0, 0, 0, 1]
                    [(int.of_nat 0, [int.of_nat 0, int.of_nat 1, -[1+ 0]]), (int.of_nat 0,
                       [int.of_nat 0, int.of_nat 1, int.of_nat 0]), (int.of_nat 0,
                       [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0],
                       [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0],
                       [int.of_nat 0, int.of_nat 0, int.of_nat 0])]
                    (omega.unsat_lin_comb_of [0, 0, 0, 0, 1]
                       [(int.of_nat 0, [int.of_nat 0, int.of_nat 1, -[1+ 0]]), (int.of_nat 0,
                          [int.of_nat 0, int.of_nat 1, int.of_nat 0]), (int.of_nat 0,
                          [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0],
                          [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0],
                          [int.of_nat 0, int.of_nat 0, int.of_nat 0])]
                       (int.neg_succ_lt_zero 0)
                       (omega.forall_mem_repeat_zero_eq_zero [int.of_nat 0, int.of_nat 0, int.of_nat 0].length))))
              (omega.clauses.unsat_cons
                 ([(int.of_nat 0, [int.of_nat 0, int.of_nat 0, -[1+ 0]])],
                  [(int.of_nat 0, [int.of_nat 1]), (int.of_nat 0, [int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                     [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0], [-[1+ 0], int.of_nat 1]), (-[1+ 0],
                     [-[1+ 0], int.of_nat 1, -[1+ 0]]), (int.of_nat 0, [int.of_nat 1, -[1+ 0]])])
                 [([(int.of_nat 0, [int.of_nat 1, -[1+ 0], int.of_nat 1])],
                    [(int.of_nat 0, [int.of_nat 1]), (int.of_nat 0, [int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                       [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0], [-[1+ 0], int.of_nat 1]), (-[1+ 0],
                       [int.of_nat 1, -[1+ 0], int.of_nat 1])]), ([(int.of_nat 0,
                       [int.of_nat 0, int.of_nat 0, -[1+ 0]])],
                    [(int.of_nat 0, [int.of_nat 1]), (int.of_nat 0, [int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                       [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0], [-[1+ 0], int.of_nat 1]), (-[1+ 0],
                       [int.of_nat 1, -[1+ 0], int.of_nat 1]), (int.of_nat 0, [int.of_nat 1, -[1+ 0]])])]
                 (omega.unsat_of_unsat_eq_elim [omega.ee.factor (int.of_nat 1), omega.ee.neg, omega.ee.cancel 2]
                    ([(int.of_nat 0, [int.of_nat 0, int.of_nat 0, -[1+ 0]])],
                     [(int.of_nat 0, [int.of_nat 1]), (int.of_nat 0, [int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                        [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0], [-[1+ 0], int.of_nat 1]), (-[1+ 0],
                        [-[1+ 0], int.of_nat 1, -[1+ 0]]), (int.of_nat 0, [int.of_nat 1, -[1+ 0]])])
                    (omega.unsat_of_unsat_lin_comb [0, 0, 0, 1, 0, 1]
                       [(int.of_nat 0, [int.of_nat 1, int.of_nat 0, int.of_nat 0]), (int.of_nat 0,
                          [int.of_nat 0, int.of_nat 1, int.of_nat 0]), (int.of_nat 0,
                          [int.of_nat 0, int.of_nat 0, int.of_nat 0]), (-[1+ 0],
                          [-[1+ 0], int.of_nat 1, int.of_nat 0]), (-[1+ 0],
                          [-[1+ 0], int.of_nat 1, int.of_nat 0]), (int.of_nat 0, [int.of_nat 1, -[1+ 0], int.of_nat 0])]
                       (omega.unsat_lin_comb_of [0, 0, 0, 1, 0, 1]
                          [(int.of_nat 0, [int.of_nat 1, int.of_nat 0, int.of_nat 0]), (int.of_nat 0,
                             [int.of_nat 0, int.of_nat 1, int.of_nat 0]), (int.of_nat 0,
                             [int.of_nat 0, int.of_nat 0, int.of_nat 0]), (-[1+ 0],
                             [-[1+ 0], int.of_nat 1, int.of_nat 0]), (-[1+ 0],
                             [-[1+ 0], int.of_nat 1, int.of_nat 0]), (int.of_nat 0,
                             [int.of_nat 1, -[1+ 0], int.of_nat 0])]
                          (int.neg_succ_lt_zero 0)
                          (omega.forall_mem_repeat_zero_eq_zero [int.of_nat 0, int.of_nat 0, int.of_nat 0].length))))
                 (omega.clauses.unsat_cons
                    ([(int.of_nat 0, [int.of_nat 1, -[1+ 0], int.of_nat 1])],
                     [(int.of_nat 0, [int.of_nat 1]), (int.of_nat 0, [int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                        [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0], [-[1+ 0], int.of_nat 1]), (-[1+ 0],
                        [int.of_nat 1, -[1+ 0], int.of_nat 1])])
                    [([(int.of_nat 0, [int.of_nat 0, int.of_nat 0, -[1+ 0]])],
                       [(int.of_nat 0, [int.of_nat 1]), (int.of_nat 0, [int.of_nat 0, int.of_nat 1]), (int.of_nat 0,
                          [int.of_nat 0, int.of_nat 0, int.of_nat 1]), (-[1+ 0], [-[1+ 0], int.of_nat 1]), (-[1+ 0],
                          [int.of_nat 1, -[1+ 0], int.of_nat 1]), (int.of_nat 0, [int.of_nat 1, -[1+ 0]])])]
                    (omega.unsat_of_unsat_eq_elim [omega.ee.factor (int.of_nat 1), omega.ee.cancel 0]
                       ([(int.of_nat 0, [int.of_nat 1, -[1+ 0], int.of_nat 1])],

[Damiano Testa]

The rewrite way:

exact (id (eq.rec (eq.refl (a + (b - a) = b)) (nat.add_sub_assoc (le_of_lt h) a).symm)).mpr
  ((id (eq.rec (eq.refl (a + b - a = b)) (nat.add_sub_cancel_left a b))).mpr (eq.refl b))

[Damiano Testa]

Patrick: library search with \le:

  exact nat.add_sub_of_le h,

lemma simple {a b c : ℕ} {h : a < b} : a + (b - a) = b :=
nat.add_sub_of_le (le_of_lt h)

[Patrick Massot]

This confirms my theory.

[Bryan Gin-ge Chen]

Marcus Rossel said:

What's omega?

In short, it solves arithmetic goals over nat and int which only involve addition. See tactic#omega for more gory details. It's unfortunately a bit slow and probably needs to be rewritten from scratch as the current state is not very maintainable.

[Bryan Gin-ge Chen]

@Damiano Testa Note that you can write h.le instead of le_of_lt h; there are a lot of similar dot notation tricks for inequalities defined starting here.

[Damiano Testa]

Bryan, thank you very much for this pointer: I had no idea of this possibility! I also think that this is the third time that someone mentions to me the dot notation: it is taking more time than I thought to really use it!

I updated the proof above, exploiting the shortening!

[Bryan Gin-ge Chen]

No problem. This one's relatively minor, but I'm a big fan of the way dot notation works in Lean; it can really make long chains of applications much shorter without sacrificing too much readability.