12 questions
- Bountied 0
- Unanswered
- Frequent
- Score
- Trending
- Week
- Month
- Unanswered (my tags)
0
votes
0
answers
31
views
How can I regroup list concatenations in an idris type?
In Idris2 I have a predicate P : List A -> Type (It is actually a typing judgement where the list is a context, but I'm keeping the question general to avoid explaining everything). I also have a ...
0
votes
0
answers
75
views
why can't i weaken my goal in coq? (beginner)
I'm quite new to Coq, I have done several projects in OCaml before and I'm doing this as a preparation for a course I'm taking next semester.
A friend recommended the exercise of proofing the ...
0
votes
0
answers
63
views
How do I fold a function over the bindings in a map in Isabelle?
What I want to be able to do is fold a function over the bindings in a map, and look up keys.
Coq has the FMap modules, is there a similar Isabelle theory module?
https://coq.inria.fr/doc/v8.19/stdlib/...
1
vote
1
answer
72
views
Understanding nat_ind2 in Logical Foundations
As an alternative induction principle of nat, nat_ind2 is defined like so:
Definition nat_ind2 :
forall (P : nat -> Prop),
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S(S n))) ->
...
0
votes
1
answer
261
views
Why does coq not recognize that `None = Some v` is false?
I have a function:
Fixpoint eval (fuel : nat) (env : environment) (e : exp) :=
match fuel with
| 0 => None
| S fuel' => (...)
end
I'm now proving a property of such ...
0
votes
2
answers
92
views
Termination checking of a function fails in Agda
I'm currently writing the following incomplete function for this project:
extend : ∀ o asc (s : CSet (suc k) o) → SC asc → SC (add s asc)
extend 0 asc s rewrite l≡0 s Eq.refl =
restrict (add (...
0
votes
1
answer
91
views
stuck on a proof (modeling IMP language)
I've been trying 'port' some of the imperative language (IMP2) formalized in Isabelle here: https://www.isa-afp.org/sessions/imp2/#Semantics.html
to Agda.
First, here are some initial translations I ...
0
votes
2
answers
127
views
True in Goal State Coq
While attempting to prove All in Software Foundations Volume 1, Logic.v, I came across a proof state of simply True. I.e. my proof state looks like:
T : Type
P : T -> Prop
H : forall x : T, False -...
0
votes
1
answer
174
views
How can I write a filter function for sequences represented as functions in Coq?
Given that we have the types T1, T2 and T_Union, as well as functions proj1 : T_Union -> option T1 and proj2 : T_Union -> option T2, and a sequence represented as nat -> T_Union, how can you ...
1
vote
1
answer
140
views
erase common constant of equation using leanprover
I want to prove below goal.
n_n: N
n_ih: n_n * (n_n + 1) / 2 = arith_sum n_n
⊢ (n_n + 1) * (n_n + 1 + 1) / 2 = n_n + 1 + n_n * (n_n + 1) / 2
ring, simp, linarith is not working.
Also I tried calc, ...
1
vote
1
answer
58
views
How does one build the list of only true elements in Coq using dependent types?
I was going through the Coq book from the maths perspective. I was trying to define a dependently typed function that returned a length list with n trues depending on the number trues we want.
Coq ...
0
votes
1
answer
352
views
How does one define dependent type with named arguments in Coq without issues in unification in the constructors?
I want to defined a lenghted list but I like arguments with names at the top of the inductive definition. Whenever I try that I get unification errors with things I hoped worked and was forced to do a ...