Questions tagged [prop]
A sort of definitionally proof-irrelevant propositions introduced in "Definitional Proof-Irrelevance without K" and implemented by Agda (as Prop) and Coq (as SProp).
10
questions
3
votes
1
answer
96
views
Coq's elimination restriction corner cases -- when can you eliminate Prop's into Type?
In order to ensure soundness, and to keep axioms like proof irrelevance admissible, Coq has an "elimination restriction" on inductive types in Prop.
...
- 98
3
votes
3
answers
225
views
Pattern matching from `Prop` to `Type` in Lean
I'm a beginner in the world of proof assistants, and have been taking a look at Lean4 lately.
I wanted to write a function like
...
1
vote
1
answer
69
views
Coq Induction on Hypothesis destroys the Hypothesis
I'm trying to prove something in coq
I have and Inductive prop type named in_order_merge which is a relation between three lists that shows third one is in_order merge of first two, here is the ...
6
votes
0
answers
147
views
How does the modality-based irrelevance compare to universe-based irrelevance (`Prop`)?
I understand proof irrelevance implementation as one of the two language features listed below:
Prop as SProp in Coq or ...
- 5,877
2
votes
0
answers
96
views
Is there a good demonstration of bidirectional type checking with strict Prop?
I've seen elaboration-zoo, pi-forall, Mini-TT, etc., all kinds of demonstrations of dependent type elaboration. However, none of them support Prop.
I am interested ...
- 5,877
5
votes
1
answer
184
views
Why can termination checker affect strict Prop in Agda?
In https://dl.acm.org/doi/10.1145/3290316 section 4 (which I believe is a standard reference), the authors claimed that Voevodsky's propositional resizing rule justifies the consistency of an ...
- 5,877
5
votes
1
answer
151
views
Is 'subsingleton elimination' the same concept as 'function comprehension'?
I saw:
subsingleton elimination from lean-forward, which, I so far understood as "eliminate a type in Prop to a type in whatever universe that we know has at ...
- 5,877
4
votes
2
answers
167
views
Turning off some sProp checks
In Definitional Proof Irrelevance Without K, inductives in sProp need to satisfy three conditions to allow large elimination:
(1) Every non-forced argument must be in sProp.
(2) The return types of ...
- 906
10
votes
1
answer
314
views
How does Prop relate to h-prop and double negation?
I'm referring to these concepts:
Prop in Agda and SProp in Coq, a "sort of definitionally proof-irrelevant propositions", and their squash type (and relatedly, the usual Prop in Coq);
mere ...
- 1,015
12
votes
3
answers
315
views
Why does it matter if canonicity holds for irrelevant types?
Suppose you were to add a non-constructive axiom which only applies to irrelevant types, such as the irrelevance axiom. To my understanding canonicity and strong normalization are defining features of ...
- 1,015