[Agda] cong with wildcard

[Sergei Meshveliani]

Dear all,

There is a problem of unnecessary large terms in proofs in a source
program. For example, in an equality proof by EquationalReasoning of

begin T1 ≡⟨ cong foo1 eq1 ⟩
T2 ≡⟨ cong foo2 eq2 ⟩
T3
...
∎

foo1, foo2 ... often occur large terms which can be replaced with `_'.
But Agda cannot solve this.
For example, for the Nat arithmetic, the line

(a * 1 + 1+m * n) ≡⟨ cong (_+ (1+m * n)) (Nat0.*1 a) ⟩

means replacing a * 1 with a.
And from the term triple

(a * 1 + 1+m * n) , (cong (_+ _) (Nat0.*1 a)) ,
(a + 1+m * n)

it is clear (to a human) which term t to substitute for `_' in order
to obtain the third term
-- provided that this t is a subterm in (a * 1 + 1+m * n).

More general: the derivation is

E1 -- cong (op _) foo -->
E2

where op is an operator, and the prover needs to search in E1 all
subterms to which (op X) matches, and which substitution derives E2.

Does there exist a library for Agda that has tools for this?
Can something easy be done towards such a tool?

Regards,

------
Sergei

[Arseniy Alekseyev]

What I found super-helpful to Agda is having the definitions of your
operators abstract, e.g. working in an arbitrary semiring instead of with
Nats directly.
Then Agda is much happier to infer things in general and I think it will
infer your example too.

Post by Sergei Meshveliani
Dear all,
There is a problem of unnecessary large terms in proofs in a source
program. For example, in an equality proof by EquationalReasoning of
begin T1 ≡⟚ cong foo1 eq1 ⟩
T2 ≡⟚ cong foo2 eq2 ⟩
T3
...
∎
foo1, foo2 ... often occur large terms which can be replaced with `_'.
But Agda cannot solve this.
For example, for the Nat arithmetic, the line
(a * 1 + 1+m * n) ≡⟚ cong (_+ (1+m * n)) (Nat0.*1 a) ⟩
means replacing a * 1 with a.
And from the term triple
(a * 1 + 1+m * n) , (cong (_+ _) (Nat0.*1 a)) ,
(a + 1+m * n)
it is clear (to a human) which term t to substitute for `_' in order
to obtain the third term
-- provided that this t is a subterm in (a * 1 + 1+m * n).
More general: the derivation is
E1 -- cong (op _) foo -->
E2
where op is an operator, and the prover needs to search in E1 all
subterms to which (op X) matches, and which substitution derives E2.
Does there exist a library for Agda that has tools for this?
Can something easy be done towards such a tool?
Regards,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Matthew Daggitt]

Also might be worth having a look at Bradley's Agda holes library (
https://github.com/bch29/agda-holes).

Post by Arseniy Alekseyev
What I found super-helpful to Agda is having the definitions of your
operators abstract, e.g. working in an arbitrary semiring instead of with
Nats directly.
Then Agda is much happier to infer things in general and I think it will
infer your example too.

Post by Sergei Meshveliani
Dear all,
There is a problem of unnecessary large terms in proofs in a source
program. For example, in an equality proof by EquationalReasoning of
begin T1 ≡⟚ cong foo1 eq1 ⟩
T2 ≡⟚ cong foo2 eq2 ⟩
T3
...
∎
foo1, foo2 ... often occur large terms which can be replaced with `_'.
But Agda cannot solve this.
For example, for the Nat arithmetic, the line
(a * 1 + 1+m * n) ≡⟚ cong (_+ (1+m * n)) (Nat0.*1 a) ⟩
means replacing a * 1 with a.
And from the term triple
(a * 1 + 1+m * n) , (cong (_+ _) (Nat0.*1 a)) ,
(a + 1+m * n)
it is clear (to a human) which term t to substitute for `_' in order
to obtain the third term
-- provided that this t is a subterm in (a * 1 + 1+m * n).
More general: the derivation is
E1 -- cong (op _) foo -->
E2
where op is an operator, and the prover needs to search in E1 all
subterms to which (op X) matches, and which substitution derives E2.
Does there exist a library for Agda that has tools for this?
Can something easy be done towards such a tool?
Regards,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

Post by Matthew Daggitt
Also might be worth having a look at Bradley's Agda holes library
(https://github.com/bch29/agda-holes).

Thank you. This may occur useful.

Of course, this can be done by developing/using a library based on
reflection.

------
Sergei

Post by Matthew Daggitt
What I found super-helpful to Agda is having the definitions
of your operators abstract, e.g. working in an arbitrary
semiring instead of with Nats directly.
Then Agda is much happier to infer things in general and I
think it will infer your example too.
On Tue, Jul 10, 2018, 12:57 Sergei Meshveliani
Dear all,
There is a problem of unnecessary large terms in
proofs in a source
program. For example, in an equality proof by
EquationalReasoning of
begin T1 ≡⟨ cong foo1 eq1 ⟩
T2 ≡⟨ cong foo2 eq2 ⟩
T3
...
∎
foo1, foo2 ... often occur large terms which can be
replaced with `_'.
But Agda cannot solve this.
For example, for the Nat arithmetic, the line
(a * 1 + 1+m * n) ≡⟨ cong (_+ (1+m * n))
(Nat0.*1 a) ⟩
means replacing a * 1 with a.
And from the term triple
(a * 1 + 1+m * n) , (cong (_+ _) (Nat0.*1 a)) ,
(a + 1+m * n)
it is clear (to a human) which term t to substitute
for `_' in order
to obtain the third term
-- provided that this t is a subterm in (a * 1 + 1+m
* n).
More general: the derivation is
E1 -- cong (op _) foo -->
E2
where op is an operator, and the prover needs to
search in E1 all
subterms to which (op X) matches, and which
substitution derives E2.
Does there exist a library for Agda that has tools for
this?
Can something easy be done towards such a tool?
Regards,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Nils Anders Danielsson]

Post by Matthew Daggitt
Also might be worth having a look at Bradley's Agda holes library
(https://github.com/bch29/agda-holes).

I suspect that this library does not work with the latest (development?)
version of Agda. (Because Holes.Term.⌞_⌟ is inlined. This can be fixed
by using the NOINLINE pragma.)

I have two tactics for automatically generating applications of
cong-like lemmas, one of which is based on Bradley Hardy's idea:

http://www.cse.chalmers.se/~nad/listings/equality/Tactic.By.html
git clone http://www.cse.chalmers.se/~nad/repos/equality/